text:
(*
  This file is part of the verified smart contract project of SECBIT Labs.

  Copyright 2018 SECBIT Labs

  Author: Haozhong Zhang

  This program is free software: you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public License
  as published by the Free Software Foundation, either version 3 of
  the License, or (at your option) any later version.

  This program is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public License
  along with this program.  If not, see <https://www.gnu.org/licenses/>.
*)

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

(* XXX: shall Model.event and .state be generated from solidity? *)
Require Import Model.

(* All notations are defined in dsl_scope. *)
Delimit Scope dsl_scope with dsl.

(* *************** *)
(* DSL definitions *)
(* *************** *)

(* Definition of the primitive DSL statements *)
Inductive PrimitiveStmt :=
| DSL_require (cond: state -> env -> message -> bool)
| DSL_emit (evt: state -> env -> message -> event)
| DSL_balances_upd (addr: 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_owner_upd (owner: state -> env -> message -> address)
| DSL_mintingFinished_upd (onoff: state -> env -> message -> bool)
| DSL_return (T: Type) (expr: state -> env -> message -> T)
| DSL_ctor
| DSL_nop.
Arguments DSL_return [T].

(* Definition of DSL statements *)
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).

(* Result of statement execution *)
Record Result: Type :=
  mk_result {
      ret_st: state;        (* ending state *)
      ret_evts: eventlist;  (* generated events *)
      ret_stopped: bool;    (* does the execution have to stop? *)
    }.
(* Shortcut definition of Result that the execution can continue *)
Definition Next (st: state) (evts: eventlist) : Result :=
  mk_result st evts false.
(* Shortcut definition of Result that the execution has to stop *)
Definition Stop (st: state) (evts: eventlist) : Result :=
  mk_result st evts true.

(* Semantics of the primitive DSL statements *)
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 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)
                (st_owner st)
                (st_mintingFinished st)
         )
         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))
                (st_owner st)
                (st_mintingFinished st)
         )
         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)
                (st_owner st)
                (st_mintingFinished 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)
                (st_owner st)
                (st_mintingFinished 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)
                (st_owner st)
                (st_mintingFinished 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)
                (st_owner st)
                (st_mintingFinished st)
         )
         evts

  | DSL_owner_upd owner =>
    Next (mk_st (st_symbol st)
                (st_name st)
                (st_decimals st)
                (st_totalSupply st)
                (st_balances st)
                (st_allowed st)
                (owner st env msg)
                (st_mintingFinished st)
         )
         evts

  | DSL_mintingFinished_upd onoff =>
    Next (mk_st (st_symbol st)
                (st_name st)
                (st_decimals st)
                (st_totalSupply st)
                (st_balances st)
                (st_allowed st)
                (st_owner st)
                (onoff st env msg)
         )
         evts

  | DSL_ctor =>
    Next st
         (evts ++ (ev_MintableToken (this)
                                    (st_totalSupply st)
                                    (st_name st)
                                    (st_decimals st)
                                    (st_symbol st) :: nil))

  | DSL_nop =>
    Next st evts
  end.

(* Semantics of DSL statements *)
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.

(* ************************************************************** *)
(* Optional notations that makes the DSL syntax close to Solidity *)
(* ************************************************************** *)

(* Notations for state variables (XXX: shall they be generated from solidity?) *)
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.

Definition dsl_balances_access (addr: state -> env -> message -> address) :=
  fun (st: state) (env: env) (msg: message) =>
    (balances%dsl st env msg) (addr st env msg).
Notation "'balances' '[' addr ']'" :=
  (dsl_balances_access addr): dsl_scope.

Notation "'allowed'" :=
  (fun (st: state) (env: env) (msg: message) => st_allowed st) : dsl_scope.

Definition dsl_allowed_access (from to: state -> env -> message -> address) :=
  fun (st: state) (env: env) (msg: message) =>
    (allowed%dsl st env msg) ((from st env msg), (to st env msg)).
Notation "'allowed' '[' from ']' '[' to ']'" :=
  (dsl_allowed_access from to): dsl_scope.

Notation "'owner'" :=
  (fun (st: state) (env: env) (msg: message) => st_owner st) : dsl_scope.

Notation "'mintingFinished'" :=
  (fun (st: state) (env: env) (msg: message) => st_mintingFinished st) : dsl_scope.

(* Notations for events (XXX: shall they be generated from solidity?) *)
Notation "'Transfer' '(' from ',' to ',' value ')'" :=
  (fun (st: state) (env: env) (msg: message) =>
     ev_Transfer (m_sender msg) (from st env msg) (to st env msg) (value st env msg))
    (at level 210): dsl_scope.

Notation "'Approval' '(' _owner ',' spender ',' value ')'" :=
  (fun (st: state) (env: env) (msg: message) =>
     ev_Approval (m_sender msg) (_owner st env msg) (spender st env msg) (value st env msg))
    (at level 210): dsl_scope.

Notation "'Mint' '(' to ',' amount ')'" :=
  (fun (st: state) (env: env) (msg: message) =>
     ev_Mint (m_sender msg) (to st env msg) (amount st env msg))
    (at level 210): dsl_scope.

Notation "'MintFinished' '(' ')'" :=
  (fun (st: state) (env: env) (msg: message) =>
     ev_MintFinished (m_sender msg))
    (at level 210): dsl_scope.

Notation "'MintFinished' '()'" :=
  (fun (st: state) (env: env) (msg: message) =>
     ev_MintFinished (m_sender msg))
    (at level 210): dsl_scope.

(* Notations for solidity expressions *)
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) =>
    plus_with_overflow (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) =>
    minus_with_underflow (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.

Definition dsl_not :=
  fun x (st: state) (env: env) (msg: message) =>
    (negb (x st env msg)).
Notation "'!' x" := (dsl_not x) (at level 75, right associativity) : dsl_scope.

Notation "'msg.sender'" :=
  (fun (st: state) (env: env) (msg: message) =>
     m_sender msg) : dsl_scope.

Definition o0 := 0.

Notation "'0'" :=
  (fun (st: state) (env: env) (msg: message) => 0) : 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.

Notation "'require' '(' cond ')'" :=
  (DSL_require cond) (at level 200) : dsl_scope.
Notation "'emit' evt" :=
  (DSL_emit evt) (at level 200) : dsl_scope.
Notation "'balances' '[' addr ']' '=' expr" :=
  (DSL_balances_upd addr expr) (at level 0) : dsl_scope.
Notation "'balances' '[' addr ']' '+=' expr" :=
  (DSL_balances_upd addr
                    (dsl_add (dsl_balances_access addr) expr))
    (at level 0) : dsl_scope.
Notation "'balances' '[' addr ']' '-=' expr" :=
  (DSL_balances_upd addr
                    (dsl_sub (dsl_balances_access addr) expr))
    (at level 0) : dsl_scope.
Notation "'allowed' '[' from ']' '[' to ']' '=' expr" :=
  (DSL_allowed_upd from to expr) (at level 0) : dsl_scope.
Notation "'allowed' '[' from ']' '[' to ']' '+=' expr" :=
  (DSL_allowed_upd from to
                   (dsl_add (dsl_allowed_access from to) expr))
    (at level 0) : dsl_scope.
Notation "'allowed' '[' from ']' '[' to ']' '-=' expr" :=
  (DSL_allowed_upd from to
                   (dsl_sub (dsl_allowed_access from to) expr))
    (at level 0) : dsl_scope.
Notation "'totalSupply' '=' expr" :=
  (DSL_totalSupply_upd expr) (at level 0) : dsl_scope.
Notation "'totalSupply' '+=' expr" :=
  (DSL_totalSupply_upd (dsl_add totalSupply%dsl expr)) (at level 0) : dsl_scope.
Notation "'totalSupply' '-=' expr" :=
  (DSL_totalSupply_upd (dsl_sub totalSupply%dsl expr)) (at level 0) : dsl_scope.
Notation "'symbol' '=' expr" :=
  (DSL_symbol_upd expr) (at level 0) : dsl_scope.
Notation "'name' '=' expr" :=
  (DSL_name_upd expr) (at level 0) : dsl_scope.
Notation "'decimals' '=' expr" :=
  (DSL_decimals_upd expr) (at level 0) : dsl_scope.
Notation "'owner' '=' expr" :=
  (DSL_owner_upd expr) (at level 0) : dsl_scope.
Notation "'mintingFinished' '=' expr" :=
  (DSL_mintingFinished_upd expr) (at level 0) : dsl_scope.
Notation "'return' expr" :=
  (DSL_return expr) (at level 200) : dsl_scope.
Notation "'nop'" :=
  (DSL_nop) (at level 200) : dsl_scope.
Notation "'ctor'" :=
  DSL_ctor (at level 200) : dsl_scope.

Notation "@ stmt_prim" :=
  (DSL_prim stmt_prim) (at level 200) : dsl_scope.

Notation "'@if' ( cond ) { stmt0 } 'else' { stmt1 }" :=
  (DSL_if cond stmt0 stmt1) (at level 210) : dsl_scope.

Notation "stmt0 ';' stmt1" :=
  (DSL_seq stmt0 stmt1) (at level 220) : dsl_scope.

Notation "'@uint256' x = expr ; stmt" :=
  (let x: state -> env -> message -> uint256 := expr in stmt)
    (at level 230, x ident) : dsl_scope.

Notation "'@address' x = expr ; stmt" :=
  (let x: state -> env -> message -> address := expr in stmt)
    (at level 230, x ident) : dsl_scope.

Notation "'@uint8' x = expr ; stmt" :=
  (let x: state -> env -> message -> uint8 := expr in stmt)
    (at level 230, x ident) : dsl_scope.

Notation "'@string' x = expr ; stmt" :=
  (let x: state -> env -> message -> string := expr in stmt)
    (at level 230, x ident) : dsl_scope.

(* *************************************************************** *)
(* Each section below represents a ERC20 function in DSL and prove *)
(* the DSL representation does implement the specification.        *)
(* *************************************************************** *)

Require Import Spec.

Definition dsl_sat_spec (fcall: mcall)
                        (fdsl: Stmt)
                        (fspec: address -> env -> message -> Spec) : Prop :=
  forall st env msg this,
    m_func msg = fcall
    -> spec_require (fspec this env msg) st
    -> forall st0 result,
      dsl_exec fdsl st0 st env msg this nil = result
      -> spec_trans (fspec this env msg) st (ret_st result)
         /\ spec_events (fspec this env msg) (ret_st result) (ret_evts result).

Section dsl_transfer_from.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  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}.

  (* Arguments are immutable, generated from solidity *)
  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}.

  (* DSL representation of transferFrom(), generated from solidity *)
  Definition transferFrom_dsl : Stmt :=
    (@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)).

  (* Auxiliary lemmas *)
  Lemma nat_nooverflow_dsl_nooverflow:
    forall (m: state -> a2v) st env msg,
      m_func msg = mc_transferFrom _from _to _value ->
      (_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.
  Proof.
    intros m st env msg Hmcall Hnat.

    apply transferFrom_value_inrange in Hmcall.
    destruct Hmcall as [_ Hvalue].

    unfold "=="%dsl, "<="%dsl, "||"%dsl, "||"%bool, "-"%dsl.
    rewrite (from_immutable st env msg),
            (to_immutable st env msg),
            (value_immutable st env msg),
            (max_uint256_immutable st env msg).
    destruct Hnat.
    - rewrite H. rewrite (Nat.eqb_refl _). reflexivity.
    - destruct H as [Hneq Hle].
      apply Nat.eqb_neq in Hneq. rewrite Hneq.
      apply Nat.leb_le in Hle.
      assert (Hlo: (MAX_UINT256 >= _value)%nat);
        auto.
      rewrite (minus_safe _ _ Hlo).
      exact Hle.
  Qed.

  (* Manually proved *)
  Lemma transferFrom_dsl_sat_spec_1:
    dsl_sat_spec (mc_transferFrom _from _to _value)
                 transferFrom_dsl
                 (funcspec_transferFrom_1 _from _to _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this Hfunc 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 Hfunc 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, dsl_balances_access 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.

    unfold dsl_allowed_access 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; clear Hexec.
    unfold "+"%dsl, "-"%dsl.
    repeat rewrite (value_immutable _ _ _).
    repeat rewrite (from_immutable _ _ _).
    repeat rewrite (to_immutable _ _ _).
    repeat (split; simpl; auto).
  Qed.

  Lemma transferFrom_dsl_sat_spec_2:
    dsl_sat_spec (mc_transferFrom _from _to _value)
                 transferFrom_dsl
                 (funcspec_transferFrom_2 _from _to _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this Hfunc 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 Hfunc 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, dsl_balances_access 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.

    unfold dsl_allowed_access 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.
    unfold "+"%dsl, "-"%dsl.
    repeat rewrite (value_immutable _ _ _).
    repeat rewrite (from_immutable _ _ _).
    repeat rewrite (to_immutable _ _ _).
    repeat (split; auto).
  Qed.

  Lemma transferFrom_cond_dec:
    forall st,
      Decidable.decidable
        (_from = _to \/ _from <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat).
  Proof.
    intros.
    apply Decidable.dec_or.
    - apply Nat.eq_decidable.
    - apply Decidable.dec_and.
      + apply neq_decidable.
      + apply Nat.le_decidable.
  Qed.

  Lemma transferFrom_cond_impl:
    forall st env msg,
      m_func msg = mc_transferFrom _from _to _value ->
      ~ (_from = _to \/ _from <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat) ->
      (((from == to)
        || ((fun (st : state) (env : Model.env) (msg : message) =>
               st_balances st (to st env msg)) <= max_uint256 - value)) st env msg) = ofalse.
  Proof.
    intros st env msg Hfunc Hneg.

    apply transferFrom_value_inrange in Hfunc.
    destruct Hfunc as [_ Hvalue].

    unfold "=="%dsl, "||"%dsl, "||"%bool, "<="%dsl, "-"%dsl.
    rewrite (from_immutable _ _ _).
    rewrite (to_immutable _ _ _).
    rewrite (value_immutable _ _ _).
    rewrite (max_uint256_immutable _ _ _).

    apply (Decidable.not_or _ _) in Hneg.
    destruct Hneg as [Hneq Hneg].

    apply Nat.eqb_neq in Hneq.
    rewrite Hneq; simpl.

    assert (Hvalue': (MAX_UINT256 >= _value)%nat);
      auto.
    rewrite (minus_safe _ _ Hvalue').

    apply (Decidable.not_and _ _ (neq_decidable _ _)) in Hneg.
    destruct Hneg.
    - apply Nat.eqb_neq in Hneq. apply H in Hneq. inversion Hneq.
    - apply not_le in H.
      apply Nat.leb_gt.
      auto.
  Qed.

  (* If no require can be satisfied, transferFrom() must revert to the initial state *)
  Lemma transferFrom_dsl_revert:
    forall st env msg this,
      m_func msg = mc_transferFrom _from _to _value ->
      ~ spec_require (funcspec_transferFrom_1 _from _to _value this env msg) st ->
      ~ spec_require (funcspec_transferFrom_2 _from _to _value this env msg) st ->
      (forall addr0 addr1, (st_allowed st (addr0, addr1) <= MAX_UINT256)%nat) ->
      forall st0 result,
        dsl_exec transferFrom_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    unfold funcspec_transferFrom_1, funcspec_transferFrom_2, ">="%nat.
    intros st env msg this Hfunc Hreq1_neg Hreq2_neg Hallwd_inv st0 result Hexec;
      simpl in Hreq1_neg, Hreq2_neg.

    assert (Hreq1_impl:
              (_value <= st_balances st _from)%nat ->
              (_from = _to \/ _from <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat) ->
              ~(_value <= st_allowed st (_from, m_sender msg) < MAX_UINT256)).
    {
      intros Hvalue.
      apply (Decidable.or_not_l_iff_1 _ _ (transferFrom_cond_dec _)).
      generalize Hvalue; clear Hvalue.
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.le_decidable _ _)).

      apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in Hreq1_neg.
      destruct Hreq1_neg.
      - left; auto.
      - apply (Decidable.not_and _ _ (transferFrom_cond_dec _)) in H.
        right; auto.
    }
    clear Hreq1_neg.

    assert (Hreq2_impl:
              (_value <= st_balances st _from)%nat ->
              (_from = _to \/ _from <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat) ->
              ~((_value <= st_allowed st (_from, m_sender msg))%nat /\
                st_allowed st (_from, m_sender msg) = MAX_UINT256)).
    {
      intros Hvalue.
      apply (Decidable.or_not_l_iff_1 _ _ (transferFrom_cond_dec _)).
      generalize Hvalue; clear Hvalue.
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.le_decidable _ _)).

      apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in Hreq2_neg.
      destruct Hreq2_neg.
      - left; auto.
      - apply (Decidable.not_and _ _ (transferFrom_cond_dec _)) in H.
        right; auto.
    }
    clear Hreq2_neg.

    simpl in Hexec.

    destruct (le_dec _value (st_balances st _from)).
    - (* balances[from] >= value *)
      generalize (Hreq1_impl l); clear Hreq1_impl; intros Hreq1_impl.
      generalize (Hreq2_impl l); clear Hreq2_impl; intros Hreq2_impl.

      apply Nat.leb_le in l.

      simpl in Hexec.
      unfold ">="%dsl, dsl_balances_access in Hexec.
      rewrite (Nat.ltb_antisym _ _) in Hexec.
      rewrite (from_immutable _ _ _) in Hexec.
      rewrite (value_immutable _ _ _) in Hexec.
      rewrite l in Hexec; simpl in Hexec.

      destruct (transferFrom_cond_dec st).
      + (* from = to \/ balances[to] < MAX_UINT256 - value *)
        generalize (Hreq1_impl H); clear Hreq1_impl; intros Hreq1_impl.
        apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in Hreq1_impl.
        assert (Himpl: (_value <= st_allowed st (_from, m_sender msg))%nat ->
                       ~ (st_allowed st (_from, m_sender msg) < MAX_UINT256)%nat).
        {
          apply Decidable.or_not_l_iff_1.
          - apply Nat.le_decidable.
          - auto.
        }
        clear Hreq1_impl; rename Himpl into Hreq1_impl.

        generalize (Hreq2_impl H); clear Hreq2_impl; intros Hreq2_impl.
        apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in Hreq2_impl.
        assert(Himpl: (_value <= st_allowed st (_from, m_sender msg))%nat ->
                      st_allowed st (_from, m_sender msg) <> MAX_UINT256).
        {
          apply Decidable.or_not_l_iff_1.
          - apply Nat.le_decidable.
          - auto.
        }
        clear Hreq2_impl; rename Himpl into Hreq2_impl.

        generalize (nat_nooverflow_dsl_nooverflow _ _ env msg Hfunc H); intros Hcond.
        unfold dsl_allowed_access in Hexec.
        rewrite Hcond in Hexec; simpl in Hexec; clear Hcond.

        rewrite (from_immutable _ _ _) in Hexec.
        rewrite (value_immutable _ _ _) in Hexec.

        destruct (le_dec _value (st_allowed st (_from, m_sender msg))).
        * (* allowed[from][msg.sender] >= value *)
          generalize (Hreq1_impl l0); clear Hreq1_impl; intros Hreq1_impl.
          generalize (Hreq2_impl l0); clear Hreq2_impl; intros Hreq2_impl.

          apply not_lt in Hreq1_impl.
          apply Nat.lt_gt_cases in Hreq2_impl.
          destruct Hreq2_impl.
          {
            unfold ">="%nat in Hreq1_impl. auto.
            apply (Nat.lt_le_trans _ _ _ H0) in Hreq1_impl.
            apply Nat.lt_irrefl in Hreq1_impl.
            inversion Hreq1_impl.
          }
          {
            generalize (Hallwd_inv _from (m_sender msg)).
            intros Hle.
            apply (Nat.le_lt_trans _ _ _ Hle) in H0.
            apply Nat.lt_irrefl in H0.
            inversion H0.
          }

        * (* allowed[from][msg.sender] < value *)
          apply not_le in n.
          apply Nat.ltb_lt in n.
          rewrite n in Hexec; simpl in Hexec.

          rewrite <- Hexec.
          split; auto.

      + (* from <> to /\ balances[to] >= MAX_UINT256 + value *)
        apply (transferFrom_cond_impl st env msg Hfunc) in H.
        rewrite H in Hexec; simpl in Hexec.

        rewrite <- Hexec.
        split; auto.

    - (* balances[from] < value *)
      apply Nat.leb_nle in n.

      simpl in Hexec.
      unfold ">="%dsl, dsl_balances_access in Hexec.
      rewrite (Nat.ltb_antisym _ _) in Hexec.
      rewrite (from_immutable _ _ _) in Hexec.
      rewrite (value_immutable _ _ _) in Hexec.
      rewrite n in Hexec; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.
  Qed.

  Close Scope dsl_scope.
End dsl_transfer_from.

Section dsl_transfer.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  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}.

  (* Arguments are immutable, generated from solidity *)
  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}.

  (* DSL representation of transfer(), generated from solidity *)
  Definition transfer_dsl : Stmt :=
    (@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)
    ).

  (* Auxiliary lemmas *)
  Lemma nat_nooverflow_dsl_nooverflow':
    forall (m: state -> a2v) st env msg,
      m_func msg = mc_transfer _to _value ->
      (m_sender msg = _to \/ (m_sender msg <> _to /\ (m st _to <= MAX_UINT256 - _value)))%nat ->
      ((msg.sender == to) ||
       ((fun st env msg => m st (to st env msg)) <= max_uint256 - value))%dsl st env msg = otrue.
  Proof.
    intros m st env msg Hfunc Hnat.

    apply transfer_value_inrange in Hfunc.
    destruct Hfunc as [_ Hvalue].

    unfold "||"%dsl, "||"%bool, "=="%dsl, "<="%dsl, "-"%dsl.
    rewrite (to_immutable st env msg),
            (max_uint256_immutable st env msg),
            (value_immutable st env msg).
    destruct Hnat.
    - rewrite H. rewrite (Nat.eqb_refl _). reflexivity.
    - destruct H as [Hneq Hle].
      apply Nat.eqb_neq in Hneq. rewrite Hneq.
      assert (Hlo: (MAX_UINT256 >= _value)%nat);
        auto.
      rewrite (minus_safe _ _ Hlo).
      apply Nat.leb_le in Hle. exact Hle.
  Qed.

  (* Manually proved *)
  Lemma transfer_dsl_sat_spec:
    dsl_sat_spec (mc_transfer _to _value)
                 transfer_dsl
                 (funcspec_transfer _to _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this Hfunc Hreq st0 result Hexec.

    unfold funcspec_transfer in Hreq; simpl in Hreq.
    destruct Hreq as [Hreq_blncs_lo Hreq_blncs_hi].
    unfold ">="%nat in Hreq_blncs_lo. apply Nat.leb_le in Hreq_blncs_lo.
    generalize(nat_nooverflow_dsl_nooverflow' _ st env msg Hfunc Hreq_blncs_hi).
    clear Hreq_blncs_hi. intros Hreq_blncs_hi.

    unfold transfer_dsl in Hexec; simpl in Hexec.
    unfold ">="%dsl, dsl_balances_access in Hexec.
    rewrite (value_immutable _ _ _) in Hexec.
    rewrite (Nat.ltb_antisym _ _) in Hexec.
    rewrite Hreq_blncs_lo in Hexec; simpl in Hexec.

    rewrite Hreq_blncs_hi in Hexec. simpl in Hexec.

    unfold funcspec_transfer.
    rewrite <- Hexec.
    unfold "+"%dsl, "-"%dsl.
    repeat rewrite (value_immutable _ _ _).
    repeat rewrite (to_immutable _ _ _).
    repeat (split; auto).
  Qed.

  Lemma transfer_cond_impl:
    forall st env msg,
      m_func msg = mc_transfer _to _value ->
      m_sender msg <> _to /\
      ~ (m_sender msg <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat) ->
      (((fun (_ : state) (_ : Model.env) (msg : message) => m_sender msg) == to)
       || ((fun (st : state) (env : Model.env) (msg : message) =>
              st_balances st (to st env msg)) <= max_uint256 - value)) st env msg = ofalse.
  Proof.
    intros st env msg Hfunc Hcond.

    apply transfer_value_inrange in Hfunc.
    destruct Hfunc as [_ Hvalue].

    unfold "=="%dsl, "||"%dsl, "||"%bool, "<="%dsl, "-"%dsl.
    rewrite (value_immutable _ _ _).
    rewrite (to_immutable _ _ _).
    rewrite (max_uint256_immutable _ _ _).
    rewrite (minus_safe _ _ Hvalue).

    destruct Hcond as [Hneq Heq].
    apply Nat.eqb_neq in Hneq; rewrite Hneq; simpl.

    apply (Decidable.not_and _ _ (neq_decidable _ _)) in Heq.
    destruct Heq.

    - apply Nat.eqb_neq in Hneq.
      apply H in Hneq; inversion Hneq.

    - apply not_le in H.
      apply Nat.leb_gt.
      auto.
  Qed.

  (* If no require can be satisfied, transfer() must revert to the initial state *)
  Lemma transfer_dsl_revert:
    forall st env msg this,
      m_func msg = mc_transfer _to _value ->
      ~ spec_require (funcspec_transfer _to _value this env msg) st ->
      forall st0 result,
        dsl_exec transfer_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this Hfunc Hreq_neg st0 result Hexec.

    simpl in Hreq_neg.

    assert (Hreq_impl:
              (_value <= st_balances st (m_sender msg))%nat ->
              ~(m_sender msg = _to \/
                m_sender msg <> _to /\ (st_balances st _to <= MAX_UINT256 - _value)%nat)).
    {
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.le_decidable _ _)).
      apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in Hreq_neg.
      auto.
    }
    clear Hreq_neg.

    simpl in Hexec.
    destruct (le_dec _value (st_balances st (m_sender msg))).
    - (* balances[msg.sender] >= value *)
      generalize (Hreq_impl l); clear Hreq_impl; intros Hreq.
      apply Decidable.not_or in Hreq.

      apply Nat.leb_le in l.

      simpl in Hexec.
      unfold ">="%dsl, dsl_balances_access in Hexec.
      rewrite (value_immutable _ _ _) in Hexec.
      rewrite (Nat.ltb_antisym _ _) in Hexec.
      rewrite l in Hexec; simpl in Hexec.

      apply (transfer_cond_impl st env msg Hfunc) in Hreq.
      rewrite Hreq in Hexec; clear Hreq; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.

    - (* balances[msg.sender] < value *)
      apply not_le in n.
      apply Nat.leb_gt in n.

      simpl in Hexec.
      unfold ">="%dsl, dsl_balances_access in Hexec.
      rewrite (value_immutable _ _ _) in Hexec.
      rewrite (Nat.ltb_antisym _ _) in Hexec.
      rewrite n in Hexec; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.
  Qed.

  Close Scope dsl_scope.
End dsl_transfer.

Section dsl_balanceOf.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{ _owner: state -> env -> message -> address }.
  Context `{ __owner: address }.

  (* Arguments are immutable, generated from solidity *)
  Context `{ owner_immutable: forall st env msg, _owner st env msg = __owner }.

  (* DSL representation of transfer(), generated from solidity *)
  Definition balanceOf_dsl : Stmt :=
    (@return balances[_owner]).

  (* Manually proved *)
  Lemma balanceOf_dsl_sat_spec:
    dsl_sat_spec (mc_balanceOf __owner)
                 balanceOf_dsl
                 (funcspec_balanceOf __owner).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hexec.
    unfold funcspec_balanceOf.
    rewrite <- Hexec.
    unfold dsl_balances_access.
    rewrite (owner_immutable _ _ _).
    repeat (split; auto).
  Qed.

  (* If no require can be satisfied, balanceOf() must revert to the initial state *)
  Lemma balanceOf_dsl_revert:
    forall st env msg this,
      m_func msg = mc_balanceOf __owner ->
      ~ spec_require (funcspec_balanceOf __owner this env msg) st ->
      forall st0 result,
        dsl_exec balanceOf_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this _ Hreq_neg st0 result Hexec.
    simpl in Hreq_neg.
    apply (proj1 Decidable.not_true_iff) in Hreq_neg.
    inversion Hreq_neg.
  Qed.

  Close Scope dsl_scope.
End dsl_balanceOf.

Section dsl_approve.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{ spender: state -> env -> message -> address }.
  Context `{ _spender: address }.
  Context `{ value: state -> env -> message -> uint256 }.
  Context `{ _value: uint256 }.

  (* Arguments are immutable, generated from solidity *)
  Context `{ spender_immutable: forall st env msg, spender st env msg = _spender }.
  Context `{ value_immutable: forall st env msg, value st env msg = _value }.

  (* DSL representation of approve(), generated from solidity *)
  Definition approve_dsl : Stmt :=
    (@allowed[msg.sender][spender] = value ;
     (@emit Approval(msg.sender, spender, value)) ;
     (@return true)
    ).

  (* Manually proved *)
  Lemma approve_dsl_sat_spec:
    dsl_sat_spec (mc_approve _spender _value)
                 approve_dsl
                 (funcspec_approve _spender _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hreq.
    simpl in Hexec.
    unfold funcspec_approve.
    rewrite <- Hexec.
    repeat rewrite (spender_immutable _ _ _).
    repeat rewrite (value_immutable _ _ _).
    repeat (split; auto).
  Qed.

  (* If no require can be satisfied, approve() must revert to the initial state *)
  Lemma approve_dsl_revert:
    forall st env msg this,
      m_func msg = mc_approve _spender _value ->
      ~ spec_require (funcspec_approve _spender _value this env msg) st ->
      forall st0 result,
        dsl_exec approve_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this _ Hreq_neg st0 result Hexec.
    simpl in Hreq_neg.
    apply (proj1 Decidable.not_true_iff) in Hreq_neg.
    inversion Hreq_neg.
  Qed.

  Close Scope dsl_scope.
End dsl_approve.

Section dsl_allowance.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{ _owner: state -> env -> message -> address }.
  Context `{ __owner: address }.
  Context `{ spender: state -> env -> message -> address }.
  Context `{ _spender: address }.

  (* Arguments are immutable, generated from solidity *)
  Context `{ _owner_immutable: forall st env msg, _owner st env msg = __owner }.
  Context `{ spender_immutable: forall st env msg, spender st env msg = _spender }.

  (* DSL representation of transfer(), generated from solidity *)
  Definition allowance_dsl : Stmt :=
    (@return allowed[_owner][spender]).

  (* Manually proved *)
  Lemma allowance_dsl_sat_spec:
    dsl_sat_spec (mc_allowance __owner _spender)
                 allowance_dsl
                 (funcspec_allowance __owner _spender).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hexec.
    unfold funcspec_allowance.
    rewrite <- Hexec.
    unfold dsl_allowed_access.
    rewrite (_owner_immutable _ _ _).
    rewrite (spender_immutable _ _ _).
    repeat (split; auto).
  Qed.

  (* If no require can be satisfied, allowance() must revert to the initial state *)
  Lemma allowance_dsl_revert:
    forall st env msg this,
      m_func msg = mc_allowance __owner _spender ->
      ~ spec_require (funcspec_allowance __owner _spender this env msg) st ->
      forall st0 result,
        dsl_exec allowance_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this _ Hreq_neg st0 result Hexec.
    simpl in Hreq_neg.
    apply (proj1 Decidable.not_true_iff) in Hreq_neg.
    inversion Hreq_neg.
  Qed.

  Close Scope dsl_scope.
End dsl_allowance.

Section dsl_constructor.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{ initialAmount : state -> env -> message -> uint256 }.
  Context `{ _initialAmount: uint256 }.
  Context `{ decimalUnits : state -> env -> message -> uint8 }.
  Context `{ _decimalUnits: uint8 }.
  Context `{ tokenName: state -> env -> message -> string }.
  Context `{ _tokenName: string }.
  Context `{ tokenSymbol: state -> env -> message -> string }.
  Context `{ _tokenSymbol: string }.

  (* Arguments are immutable, generated from solidity *)
  Context `{ initialAmount_immutable: forall st env msg, initialAmount st env msg = _initialAmount }.
  Context `{ decimalUnits_immutable: forall st env msg, decimalUnits st env msg = _decimalUnits }.
  Context `{ tokenName_immutable: forall st env msg, tokenName st env msg = _tokenName }.
  Context `{ tokenSymbol_immutable: forall st env msg, tokenSymbol st env msg = _tokenSymbol }.

  (* DSL representation of constructor, generated from solidity *)
  Definition ctor_dsl : Stmt :=
    (@balances[msg.sender] = initialAmount ;
     @totalSupply = initialAmount ;
     @name = tokenName ;
     @decimals = decimalUnits ;
     @symbol = tokenSymbol ;
     @owner = msg.sender ;
     @mintingFinished = false ;
     @ctor
    ).

  (* Manually proved *)
  Lemma ctor_dsl_sat_spec:
    forall st,
      st_balances st = $0 ->
      st_allowed st = $0 ->
      forall env msg this,
        m_func msg = mc_MintableToken _initialAmount _tokenName _decimalUnits _tokenSymbol ->
        spec_require (funcspec_MintableToken _initialAmount _tokenName _decimalUnits _tokenSymbol this env msg) st ->
        forall st0 result,
          dsl_exec ctor_dsl st0 st env msg this nil = result ->
          spec_trans (funcspec_MintableToken _initialAmount _tokenName _decimalUnits _tokenSymbol this env msg) st (ret_st result) /\
          spec_events (funcspec_MintableToken _initialAmount _tokenName _decimalUnits _tokenSymbol this env msg) (ret_st result) (ret_evts result).
  Proof.
    intros st Hblns_init Hallwd_init env msg this _ Hreq st0 result Hexec.

    simpl in Hexec.
    unfold funcspec_MintableToken.
    rewrite <- Hexec.
    repeat rewrite (initialAmount_immutable _ _ _).
    repeat rewrite (decimalUnits_immutable _ _ _).
    repeat rewrite (tokenName_immutable _ _ _).
    repeat rewrite (tokenSymbol_immutable _ _ _).
    rewrite Hblns_init.
    rewrite Hallwd_init.
    repeat (split; auto).
  Qed.

  Close Scope dsl_scope.
End dsl_constructor.

Section dsl_increaseApproval.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{spender: state -> env -> message -> address}.
  Context `{_spender: address}.
  Context `{value: state -> env -> message -> uint256}.
  Context `{_value: uint256}.
  Context `{max_uint256: state -> env -> message -> uint256}.

  (* Arguments are immutable, generated from solidity *)
  Context `{spender_immutable: forall st env msg, spender st env msg = _spender}.
  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}.

  (* DSL representation of constructor, generated from solidity *)
  Definition increaseApproval_dsl : Stmt :=
    (@require(allowed[msg.sender][spender] <= max_uint256 - value) ;
     @allowed[msg.sender][spender] += value ;
     (@emit Approval(msg.sender, spender, allowed[msg.sender][spender])) ;
     (@return true)
    ).

  Lemma increaseApproval_dsl_sat_spec:
    dsl_sat_spec (mc_increaseApproval _spender _value)
                 increaseApproval_dsl
                 (funcspec_increaseApproval _spender _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this Hcall Hreq st0 result Hexec.

    apply increaseApproval_value_inrange in Hcall.
    destruct Hcall as [_ Hvalue].

    simpl in Hreq. rename Hreq into Hallowed.
    apply Nat.leb_le in Hallowed.

    simpl in Hexec.
    unfold "<="%dsl, "-"%dsl, dsl_allowed_access in Hexec.
    rewrite (spender_immutable _ _ _) in Hexec.
    rewrite (value_immutable _ _ _) in Hexec.
    rewrite (max_uint256_immutable _ _ _) in Hexec.
    rewrite (minus_safe _ _ Hvalue) in Hexec.
    rewrite Hallowed in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    unfold "+"%dsl, "-"%dsl.
    repeat rewrite (spender_immutable _ _ _).
    repeat rewrite (value_immutable _ _ _).
    repeat (split; simpl; auto).
  Qed.

  (* If no require can be satisfied, increaseApproval() must revert to the initial state *)
  Lemma increaseApproval_dsl_revert:
    forall st env msg this,
      m_func msg = mc_increaseApproval _spender _value ->
      ~ spec_require (funcspec_increaseApproval _spender _value this env msg) st ->
      forall st0 result,
        dsl_exec increaseApproval_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this Hcall Hreq_neg st0 result Hexec.

    apply increaseApproval_value_inrange in Hcall.
    destruct Hcall as [_ Hvalue].

    simpl in Hreq_neg.
    apply Nat.leb_nle in Hreq_neg.

    simpl in Hexec.
    unfold "<="%dsl, "-"%dsl, dsl_allowed_access in Hexec.
    rewrite (spender_immutable _ _ _) in Hexec.
    rewrite (value_immutable _ _ _) in Hexec.
    rewrite (max_uint256_immutable _ _ _) in Hexec.
    rewrite (minus_safe _ _ Hvalue) in Hexec.
    rewrite Hreq_neg in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    split; auto.
  Qed.

  Close Scope dsl_scope.
End dsl_increaseApproval.

Section dsl_decreaseApproval.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{spender: state -> env -> message -> address}.
  Context `{_spender: address}.
  Context `{value: state -> env -> message -> uint256}.
  Context `{_value: uint256}.
  Context `{max_uint256: state -> env -> message -> uint256}.

  (* Arguments are immutable, generated from solidity *)
  Context `{spender_immutable: forall st env msg, spender st env msg = _spender}.
  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}.

  (* DSL representation of constructor, generated from solidity *)
  Definition decreaseApproval_dsl : Stmt :=
    (@uint256 oldValue = allowed[msg.sender][spender] ;
     @if (oldValue < value) {
         (@allowed[msg.sender][spender] = 0)
     } else {
         (@allowed[msg.sender][spender] -= value)
     } ;
     (@emit Approval(msg.sender, spender, allowed[msg.sender][spender])) ;
     (@return true)
    ).

  Lemma decreaseApproval_dsl_sat_spec_1:
    dsl_sat_spec (mc_decreaseApproval _spender _value)
                 decreaseApproval_dsl
                 (funcspec_decreaseApproval_1 _spender _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hreq.
    apply Nat.ltb_lt in Hreq.

    simpl in Hexec.
    unfold dsl_allowed_access, "<"%dsl in Hexec.
    rewrite (spender_immutable _ _ _) in Hexec.
    rewrite (value_immutable _ _ _) in Hexec.
    rewrite Hreq in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    repeat rewrite (spender_immutable _ _ _).
    repeat (split; simpl; auto).
    rewrite <- (tmap_get_upd_eq (st_allowed st) (m_sender msg, _spender) 0%nat) at 2.
    reflexivity.
  Qed.

  Lemma decreaseApproval_dsl_sat_spec_2:
    dsl_sat_spec (mc_decreaseApproval _spender _value)
                 decreaseApproval_dsl
                 (funcspec_decreaseApproval_2 _spender _value).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hreq.
    apply Nat.leb_le in Hreq.

    simpl in Hexec.
    unfold dsl_allowed_access, "<"%dsl in Hexec.
    rewrite (spender_immutable _ _ _) in Hexec.
    rewrite (value_immutable _ _ _) in Hexec.
    rewrite (Nat.ltb_antisym _ _) in Hexec.
    rewrite Hreq in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    unfold "-"%dsl.
    repeat rewrite (spender_immutable _ _ _).
    repeat rewrite (value_immutable _ _ _).
    repeat (split; simpl; auto).
  Qed.

  (* If no require can be satisfied, decreaseApproval() must revert to the initial state *)
  Lemma decreaseApproval_dsl_revert:
    forall st env msg this,
      m_func msg = mc_decreaseApproval _spender _value ->
      ~ spec_require (funcspec_decreaseApproval_1 _spender _value this env msg) st ->
      ~ spec_require (funcspec_decreaseApproval_2 _spender _value this env msg) st ->
      forall st0 result,
        dsl_exec decreaseApproval_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this _ Hreq_1 Hreq_2 st0 result Hexec.
    simpl in Hreq_1. simpl in Hreq_2.
    apply Nat.nlt_ge in Hreq_1.
    apply Hreq_2 in Hreq_1; inversion Hreq_1.
  Qed.

  Close Scope dsl_scope.
End dsl_decreaseApproval.

Section dsl_mint.
  Open Scope dsl_scope.

  (* Declare arguments, generated from solidity *)
  Context `{ to: state -> env -> message -> address }.
  Context `{ _to: address }.
  Context `{ amount: state -> env -> message -> uint256 }.
  Context `{ _amount: uint256 }.
  Context `{ max_uint256: state -> env -> message -> uint256 }.

  (* Arguments are immutable, generated from solidity *)
  Context `{ to_immutable: forall st env msg, to st env msg = _to }.
  Context `{ amount_immutable: forall st env msg, amount st env msg = _amount }.
  Context `{ max_uint256_immutable: forall st env msg, max_uint256 st env msg = MAX_UINT256 }.

  (* DSL representation of constructor, generated from solidity *)
  Definition mint_dsl : Stmt :=
    (@require(owner == msg.sender) ;
     @require(!mintingFinished) ;
     @require(totalSupply <= max_uint256 - amount) ;
     @require(balances[to] <= max_uint256 - amount);
     @totalSupply += amount ;
     @balances[to] += amount ;
     (@emit Mint(to, amount)) ;
     (@emit Transfer(0, to, amount)) ;
     (@return true)
    ).

  Lemma mint_dsl_sat_spec:
    dsl_sat_spec (mc_mint _to _amount)
                 mint_dsl
                 (funcspec_mint _to _amount).
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this Hcall Hreq st0 result Hexec.

    apply mint_amount_inrange in Hcall.
    destruct Hcall as [_ Hamount].

    simpl in Hreq.
    destruct Hreq as [Howner [Hmint [Htotal Hbalances]]].
    apply Nat.leb_le in Htotal.
    apply Nat.leb_le in Hbalances.

    simpl in Hexec.
    unfold "=="%dsl in Hexec.
    rewrite Howner in Hexec; rewrite (Nat.eqb_refl _) in Hexec; simpl in Hexec.

    unfold "!"%dsl in Hexec.
    rewrite Hmint in Hexec; simpl in Hexec.

    unfold "<="%dsl, "-"%dsl in Hexec.
    rewrite (amount_immutable _ _ _) in Hexec.
    rewrite (max_uint256_immutable _ _ _) in Hexec.
    rewrite (minus_safe _ _ Hamount) in Hexec.
    rewrite Htotal in Hexec; simpl in Hexec.

    unfold "<="%dsl, "-"%dsl, dsl_balances_access in Hexec.
    rewrite (to_immutable _ _ _) in Hexec.
    rewrite (amount_immutable _ _ _) in Hexec.
    rewrite (max_uint256_immutable _ _ _) in Hexec.
    rewrite (minus_safe _ _ Hamount) in Hexec.
    rewrite Hbalances in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    unfold "+"%dsl, "-"%dsl.
    repeat rewrite (to_immutable _ _ _).
    repeat rewrite (amount_immutable _ _ _).
    repeat rewrite (max_uint256_immutable _ _ _).
    repeat (split; simpl; auto).
    apply Nat.leb_le in Htotal.
    rewrite (plus_safe_lt _ _ Htotal); auto.
  Qed.

  (* If no require can be satisfied, mint() must revert to the initial state *)
  Lemma mint_dsl_revert:
    forall st env msg this,
      m_func msg = mc_mint _to _amount ->
      ~ spec_require (funcspec_mint _to _amount this env msg) st ->
      forall st0 result,
        dsl_exec mint_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this Hcall Hreq_neg st0 result Hexec.

    apply mint_amount_inrange in Hcall.
    destruct Hcall as [_ Hamount].

    simpl in Hreq_neg.
    assert (Hreq_impl: st_owner st = m_sender msg ->
                       st_mintingFinished st = ofalse ->
                       (st_totalSupply st <= MAX_UINT256 - _amount)%nat ->
                       ~(st_balances st _to <= MAX_UINT256 - _amount)%nat).
    {
      intros Howner Hmint.
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.le_decidable _ _)).

      generalize Hmint; clear Hmint.
      apply (Decidable.or_not_l_iff_1 _ _ (beq_decidable _ _)).

      generalize Howner; clear Howner.
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.eq_decidable _ _)).

      apply (Decidable.not_and _ _ (Nat.eq_decidable _ _)) in Hreq_neg.
      destruct Hreq_neg.
      - left; auto.
      - apply (Decidable.not_and _ _ (beq_decidable _ _)) in H.
        destruct H.
        + right; left; auto.
        + apply (Decidable.not_and _ _ (Nat.le_decidable _ _)) in H.
          right; right; auto.
    }
    clear Hreq_neg.

    simpl in Hexec.

    unfold "=="%dsl in Hexec.
    destruct (Nat.eq_dec (st_owner st) (m_sender msg)).
    - (* owner == msg.sender *)
      generalize (Hreq_impl e); clear Hreq_impl; intros Hreq_impl.

      rewrite e in Hexec.
      rewrite (Nat.eqb_refl _) in Hexec; simpl in Hexec.

      unfold "!"%dsl in Hexec.
      destruct (bool_dec (st_mintingFinished st) ofalse).
      + (* mintingFinished == false *)
        generalize (Hreq_impl e0); clear Hreq_impl; intros Hreq_impl.
        rewrite e0 in Hexec; simpl in Hexec.

        unfold "<="%dsl, "-"%dsl in Hexec.
        rewrite (amount_immutable _ _ _) in Hexec.
        rewrite (max_uint256_immutable _ _ _) in Hexec.
        rewrite (minus_safe _ _ Hamount) in Hexec.

        destruct (le_dec (st_totalSupply st) (MAX_UINT256 - _amount)%nat).
        * (* totalSupply <= MAX_UINT256 - amount *)
          generalize (Hreq_impl l); clear Hreq_impl; intros Hreq_impl.
          apply Nat.leb_nle in Hreq_impl.
          apply Nat.leb_le in l.
          rewrite l in Hexec; simpl in Hexec.

          unfold dsl_balances_access in Hexec.
          rewrite (to_immutable _ _ _) in Hexec.
          rewrite (max_uint256_immutable _ _ _) in Hexec.
          rewrite (amount_immutable _ _ _) in Hexec.
          rewrite (minus_safe _ _ Hamount) in Hexec.
          rewrite Hreq_impl in Hexec; simpl in Hexec.

          rewrite <- Hexec.
          split; auto.

        * (* totalSupply > MAX_UINT256 - amount *)
          apply Nat.leb_nle in n.
          rewrite n in Hexec; simpl in Hexec.

          rewrite <- Hexec.
          split; auto.

      + (* mintingFinished == true *)
        apply not_false_is_true in n.
        rewrite n in Hexec; simpl in Hexec.

        rewrite <- Hexec.
        split; auto.

    - (* owner != msg.sender *)
      apply Nat.eqb_neq in n.
      rewrite n in Hexec; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.
  Qed.

  Close Scope dsl_scope.
End dsl_mint.

Section dsl_finishMinting.
  Open Scope dsl_scope.

  (* DSL representation of constructor, generated from solidity *)
  Definition finishMinting_dsl : Stmt :=
    (@require(msg.sender == owner) ;
     @require(!mintingFinished) ;
     @mintingFinished = true ;
     (@emit MintFinished()) ;
     (@return true)
    ).

  Lemma finishMinting_dsl_sat_spec:
    dsl_sat_spec mc_finishMinting
                 finishMinting_dsl
                 funcspec_finishMinting.
  Proof.
    unfold dsl_sat_spec.
    intros st env msg this _ Hreq st0 result Hexec.

    simpl in Hreq.
    destruct Hreq as [Howner Hmint].

    simpl in Hexec.
    unfold "=="%dsl in Hexec.
    rewrite Howner in Hexec; rewrite (Nat.eqb_refl _) in Hexec; simpl in Hexec.

    unfold "!"%dsl in Hexec.
    rewrite Hmint in Hexec; simpl in Hexec.

    rewrite <- Hexec.
    repeat (split; auto).
  Qed.

  (* If no require can be satisfied, finishMinting() must revert to the initial state *)
  Lemma finishMinting_dsl_revert:
    forall st env msg this,
      m_func msg = mc_finishMinting ->
      ~ spec_require (funcspec_finishMinting this env msg) st ->
      forall st0 result,
        dsl_exec finishMinting_dsl st0 st env msg this nil = result ->
        result = Stop st0 (ev_revert this :: nil).
  Proof.
    intros st env msg this _ Hreq_neg st0 result Hexec.

    simpl in Hreq_neg.
    assert (Hreq_impl: st_owner st = m_sender msg -> ~ (st_mintingFinished st = ofalse)).
    {
      apply (Decidable.not_and _ _ (Nat.eq_decidable _ _)) in Hreq_neg.
      apply (Decidable.or_not_l_iff_1 _ _ (Nat.eq_decidable _ _)); auto.
    }

    simpl in Hexec.
    unfold "=="%dsl in Hexec.
    destruct (Nat.eq_dec (st_owner st) (m_sender msg)).
    - (* owner == msg.sender *)
      generalize (Hreq_impl e); clear Hreq_impl; intros Hreq_impl.
      rewrite e in Hexec; rewrite (Nat.eqb_refl _) in Hexec; simpl in Hexec.

      unfold "!"%dsl in Hexec.
      apply not_false_is_true in Hreq_impl.
      rewrite Hreq_impl in Hexec; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.

    - (* owner != msg.sender *)
      apply Nat.eqb_neq in n.
      rewrite (Nat.eqb_sym _ _) in Hexec.
      rewrite n in Hexec; simpl in Hexec.

      rewrite <- Hexec.
      split; auto.
  Qed.

  Close Scope dsl_scope.
End dsl_finishMinting.

author: sec-bit

repo: tokenlibs-with-proofs


text:
Require Import Events.
Require Import Memory.
Require Import Coqlib.
Require Import Values.
Require Import Maps.
Require Import Integers.
Require Import AST.
Require Import Globalenvs.
Require Import Axioms.

Require Import mem_lemmas. (*needed for definition of mem_forward etc*)
Require Import semantics.
Require Import effect_semantics.
Require Import structured_injections.
Require Import reach.
Require Import simulations.

Definition FLIP mu :=
  match mu with
    Build_SM_Injection locBSrc locBTgt pSrc pTgt local extBSrc extBTgt fSrc fTgt extern =>
    Build_SM_Injection extBSrc extBTgt fSrc fTgt extern locBSrc locBTgt pSrc pTgt local
  end.

Lemma SAWP_wd: forall mu (WD: SM_wd mu), SM_wd (FLIP mu).
Proof.
intros.
destruct mu; simpl in *.
destruct WD.
split; intros; simpl in *; try solve[auto].
  destruct (disjoint_extern_local_Src b); intuition.
  destruct (disjoint_extern_local_Tgt b); intuition.
  apply (extern_DomRng _ _ _ H).
  apply (local_DomRng _ _ _ H).
Qed.

Lemma FLIPlocBlocksSrc: forall mu,
  locBlocksSrc (FLIP mu) = extBlocksSrc mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPlocBlocksTgt: forall mu,
  locBlocksTgt (FLIP mu) = extBlocksTgt mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPextBlocksSrc: forall mu,
  extBlocksSrc (FLIP mu) = locBlocksSrc mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPextBlocksTgt: forall mu,
  extBlocksTgt (FLIP mu) = locBlocksTgt mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPpubBlocksSrc: forall mu,
  pubBlocksSrc (FLIP mu) = frgnBlocksSrc mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPpubBlocksTgt: forall mu,
  pubBlocksTgt (FLIP mu) = frgnBlocksTgt mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPfrgnBlocksSrc: forall mu,
  frgnBlocksSrc (FLIP mu) = pubBlocksSrc mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPfrgnBlocksTgt: forall mu,
  frgnBlocksTgt (FLIP mu) = pubBlocksTgt mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPlocal: forall mu,
  local_of (FLIP mu) = extern_of mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma FLIPextern: forall mu,
  extern_of (FLIP mu) = local_of mu.
Proof. intros. destruct mu; reflexivity. Qed.

Lemma RelyGuaranteeSrc: forall mu (WD: SM_wd mu) Esrc m m'
              (SrcHyp: forall b ofs, Esrc b ofs = true ->
                                     vis mu b = true)
               (Unch: Mem.unchanged_on (fun b z => Esrc b z = false) m m'),
         Mem.unchanged_on (fun b ofs => locBlocksSrc (FLIP mu) b = true /\
                                        pubBlocksSrc (FLIP mu) b = false) m m'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption.
  intros. simpl.
  rewrite FLIPlocBlocksSrc, FLIPpubBlocksSrc in H.
  case_eq (Esrc b ofs); intros; trivial; simpl in *.
  destruct H.
  destruct (disjoint_extern_local_Src _ WD b).
  apply SrcHyp in H0. unfold vis in H0. rewrite H2, H1 in H0. discriminate.
  congruence.
Qed.

Lemma unchanged_on_perm: forall (P:block -> Z -> Prop) m m'
      (Unch: Mem.unchanged_on P m m'),
      Mem.unchanged_on (fun b z => P b z /\ Mem.perm m b z Max Nonempty) m m'.
Proof. intros.
split; intros; eapply Unch; eauto.
apply H. apply H.
Qed.

Lemma unchanged_on_perm': forall (P:block -> Z -> Prop) m m'
      (Unch: Mem.unchanged_on (fun b z => P b z \/ ~ Mem.perm m b z Max Nonempty) m m'),
      Mem.unchanged_on P m m'.
Proof. intros.
split; intros; eapply Unch; eauto.
Qed.

Lemma RelyGuaranteeTgtPerm: forall mu Etgt Esrc m2 m2' (WD: SM_wd mu) m1
            (TgtHyp: forall b ofs, Etgt b ofs = true ->
                       (Mem.valid_block m2 b /\
                         (locBlocksTgt mu b = false ->
                           exists b1 delta1, foreign_of mu b1 = Some(b,delta1) /\
                           Esrc b1 (ofs-delta1) = true /\ Mem.perm m1 b1 (ofs-delta1) Max Nonempty)))
            (Unch2: Mem.unchanged_on (fun b z => Etgt b z = false) m2 m2')
            (SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)
            (*m1 (SrcPerm: forall b1 z, Esrc b1 z = true -> Mem.perm m1 b1 z Max Nonempty)*),
            Mem.unchanged_on (local_out_of_reach (FLIP mu) m1) m2 m2'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption; clear Unch2.
  intros. simpl.
  case_eq (Etgt b ofs); intros; trivial.
  destruct (TgtHyp _ _ H0) as [VB2 F]; clear TgtHyp.
  destruct H.
  rewrite FLIPlocBlocksTgt in H.
  destruct F as [b1 [d1 [Frg [ES P]]]].
    apply (extBlocksTgt_locBlocksTgt _ WD _ H).
  destruct (H1 b1 d1); clear H1.
     rewrite FLIPlocal.
     apply foreign_in_extern; assumption.
     congruence.
  rewrite FLIPpubBlocksSrc in H2.
    apply (foreign_DomRng _ WD) in Frg. intuition.
    rewrite H6 in H2. inv H2.
Qed.

Lemma RelyGuaranteeTgt: forall mu Etgt Esrc m2 m2' (WD: SM_wd mu)
            (TgtHyp: forall b ofs, Etgt b ofs = true ->
                       (Mem.valid_block m2 b /\
                         (locBlocksTgt mu b = false ->
                           exists b1 delta1, foreign_of mu b1 = Some(b,delta1) /\
                           Esrc b1 (ofs-delta1) = true)))
            (Unch2: Mem.unchanged_on (fun b z => Etgt b z = false) m2 m2')
            (SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)
            m1 (SrcPerm: forall b1 z, Esrc b1 z = true -> Mem.perm m1 b1 z Max Nonempty),
            Mem.unchanged_on (local_out_of_reach (FLIP mu) m1) m2 m2'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption; clear Unch2.
  intros. simpl. rename b into b2.
  case_eq (Etgt b2 ofs); intros; trivial.
  destruct (TgtHyp _ _ H0) as [VB2 F]; clear TgtHyp.
  destruct H.
  rewrite FLIPlocBlocksTgt in H.
  destruct F as [b1 [d1 [Frg ES]]].
    apply (extBlocksTgt_locBlocksTgt _ WD _ H).
  rewrite FLIPlocal in H1.
  destruct (foreign_DomRng _ WD _ _ _ Frg) as [AA [BB [CC [DD [EE [FF [GG HH]]]]]]].
(*  apply SrcHyp in ES. unfold vis in ES.
    rewrite CC in ES; simpl in ES.(* rewrite H2 in *. inv CC.*)*)
  specialize (SrcPerm _ _ ES).
  destruct (H1 b1 d1); clear H1.
     apply foreign_in_extern; assumption.
     contradiction.
  rewrite FLIPpubBlocksSrc in H2. congruence.
Qed.

(*Once these RG results are used in a linker/concurrency machine,
  we will need to remove all blocks b with isGlobalBlock ge from pubBlocks*)
Lemma RGSrc_multicore: forall mu Esrc m m'
         (SrcHyp: forall b ofs, Esrc b ofs = true -> Mem.valid_block m b -> vis mu b = true)
         (Unch: Mem.unchanged_on (fun b z => Esrc b z = false) m m')
          nu
         (VAL: smvalid_src nu m)
         (LB: forall b, locBlocksSrc nu b = true -> locBlocksSrc mu b = false)
         (PB: forall b, frgnBlocksSrc mu b && locBlocksSrc nu b = true ->
                        pubBlocksSrc nu b = true),
         Mem.unchanged_on (fun b ofs => locBlocksSrc nu b = true /\
                                        pubBlocksSrc nu b = false) m m'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption.
  intros b1 ofs H2. simpl.
  case_eq (Esrc b1 ofs); intros; trivial; simpl in *.
  apply SrcHyp in H. unfold vis in H.
  clear Unch SrcHyp.
  destruct H2.
  rewrite LB in H; trivial; clear LB.
  rewrite PB in H1; trivial. intuition.
  destruct H2.
  apply (VAL b1). unfold DOM, DomSrc. rewrite H0; auto.
Qed.

Lemma RGSrc_multicore'': forall mu Esrc m m'
         (SrcHyp: forall b ofs, Esrc b ofs = true -> Mem.valid_block m b -> vis mu b = true)
         (Unch: Mem.unchanged_on (fun b z => Esrc b z = false) m m')
          nu
(*         (VAL: smvalid_src nu m)*)
         (LB: forall b, locBlocksSrc nu b = true -> locBlocksSrc mu b = false)
         (PB: forall b, frgnBlocksSrc mu b && locBlocksSrc nu b = true ->
                        pubBlocksSrc nu b = true),
         Mem.unchanged_on (fun b ofs => locBlocksSrc nu b = true /\
                                        pubBlocksSrc nu b = false) m m'.
Proof. intros.
  eapply unchanged_on_validblock; try eassumption.
  intros b1 ofs VAL H2. simpl.
  case_eq (Esrc b1 ofs); intros; trivial; simpl in *.
  apply SrcHyp in H; trivial. unfold vis in H.
  clear Unch SrcHyp.
  destruct H2.
  rewrite LB in H; trivial; clear LB.
  rewrite PB in H1; trivial. intuition.
Qed.

Lemma RGSrc_multicore': forall mu (WDmu: SM_wd mu) Esrc m m'
         (SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)
         (Unch: Mem.unchanged_on (fun b z => Esrc b z = false) m m')
          nu (WDnu: SM_wd nu)
         (LB: forall b, locBlocksSrc nu b = true -> locBlocksSrc mu b = false)
         (X2: forall b1 b2 d, foreign_of mu b1 = Some(b2, d) ->
                              locBlocksSrc nu b1 || locBlocksTgt nu b2 = true ->
                              pub_of nu b1 = Some(b2,d)),
         Mem.unchanged_on (fun b ofs => locBlocksSrc nu b = true /\
                                        pubBlocksSrc nu b = false) m m'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption.
  intros b1 ofs H2. simpl.
  case_eq (Esrc b1 ofs); intros; trivial; simpl in *.
  apply SrcHyp in H. unfold vis in H.
  clear Unch SrcHyp.
  destruct H2.
  rewrite LB in H; trivial; clear LB.
  simpl in H.
  destruct (frgnSrc _ WDmu _ H) as [b2 [d [Frg FT]]].
  apply X2 in Frg.
     destruct (pubChar _ WDnu _ _ _ Frg).
     rewrite H1 in H2. discriminate.
  rewrite H0; reflexivity.
Qed.

Lemma RGSrc_multicoreLICSpaper: forall mu (WDmu: SM_wd mu) Esrc m m'
         (SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)
         (Unch: Mem.unchanged_on (fun b z => Esrc b z = false) m m')
          nu (WDnu: SM_wd nu)
         (LB: forall b, locBlocksSrc nu b = true -> locBlocksSrc mu b = true -> False)
         (X2: forall b1 b2 d, foreign_of mu b1 = Some(b2, d) ->
                              locBlocksSrc nu b1 || locBlocksTgt nu b2 = true ->
                              pub_of nu b1 = Some(b2,d)),
         Mem.unchanged_on (fun b ofs => locBlocksSrc nu b = true /\
                                        pubBlocksSrc nu b = false) m m'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption.
  intros b1 ofs H2. simpl.
  case_eq (Esrc b1 ofs); intros; trivial; simpl in *.
  apply SrcHyp in H. unfold vis in H.
  clear Unch SrcHyp.
  destruct H2.
  specialize (LB b1 H0).
  remember (locBlocksSrc mu b1) as d.
  destruct d; simpl in *; try contradiction. clear LB.
  destruct (frgnSrc _ WDmu _ H) as [b2 [d [Frg FT]]].
  apply X2 in Frg.
     destruct (pubChar _ WDnu _ _ _ Frg).
     rewrite H1 in H2. discriminate.
  rewrite H0; reflexivity.
Qed.

Lemma RGTgt_multicore: forall mu Etgt Esrc m2 m2' (WD: SM_wd mu)
            (TgtHyp: forall b ofs, Etgt b ofs = true ->
                       (Mem.valid_block m2 b /\
                         (locBlocksTgt mu b = false ->
                           exists b1 delta1, foreign_of mu b1 = Some(b,delta1) /\
                           Esrc b1 (ofs-delta1) = true)))
            (Unch2: Mem.unchanged_on (fun b z => Etgt b z = false) m2 m2')
            (*(SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)*)
            m1 (SrcPerm: forall b1 z, Esrc b1 z = true -> Mem.perm m1 b1 z Max Nonempty)
            nu
         (X1: forall b, locBlocksTgt nu b = true -> locBlocksTgt mu b = false)
         (X2: forall b1 b2 d, foreign_of mu b1 = Some(b2, d) ->
                              locBlocksSrc nu b1 || locBlocksTgt nu b2 = true ->
                              pub_of nu b1 = Some(b2,d)),
            Mem.unchanged_on (local_out_of_reach nu m1) m2 m2'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption; clear Unch2.
  intros. simpl. rename b into b2.
  case_eq (Etgt b2 ofs); intros; trivial.
  destruct (TgtHyp _ _ H0) as [VB2 F]; clear TgtHyp.
  destruct H.
  specialize (X1 _ H).
  destruct (F X1) as [b1 [d1 [Frg ES]]]; clear F.
  destruct (foreign_DomRng _ WD _ _ _ Frg) as [AA [BB [CC [DD [EE [FF [GG HH]]]]]]].
  clear DD.
(*  apply SrcHyp in ES. clear SrcHyp.
    rewrite H2 in *. inv CC.
  clear H2.*)
  specialize (X2 _ _ _ Frg). rewrite H in X2.
  rewrite orb_true_r in X2. specialize (X2 (eq_refl _)).
  destruct (H1 b1 d1).
    apply pub_in_local. apply X2.
    specialize (SrcPerm _ _ ES). contradiction.
  rewrite (pubSrcContra _ _ H2) in X2. inv X2.
Qed.

Lemma RGTgt_multicorePerm': forall mu Etgt Esrc m2 m2' (WD: SM_wd mu) m1
            (TgtHyp: forall b ofs, Etgt b ofs = true ->
                       (Mem.valid_block m2 b /\
                         (locBlocksTgt mu b = false ->
                           exists b1 delta1, foreign_of mu b1 = Some(b,delta1) /\
                           Esrc b1 (ofs-delta1) = true /\ Mem.perm m1 b1 (ofs-delta1) Max Nonempty)))
            (Unch2: Mem.unchanged_on (fun b z => Etgt b z = false) m2 m2')
            nu (WDnu: SM_wd nu) (AI: inject_incr (as_inj nu) (as_inj mu))
             (SEP: sm_inject_separated nu mu m1 m2)
         (X1: forall b, locBlocksTgt nu b = true -> locBlocksTgt mu b = false)
         (PB: forall b, frgnBlocksSrc mu b && locBlocksSrc nu b = true ->
                        pubBlocksSrc nu b = true),
            Mem.unchanged_on (local_out_of_reach nu m1) m2 m2'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption; clear Unch2.
  intros. simpl. rename b into b2.
  case_eq (Etgt b2 ofs); intros; trivial.
  destruct (TgtHyp _ _ H0) as [VB2 F]; clear TgtHyp.
  destruct H.
  specialize (X1 _ H).
  destruct (F X1) as [b1 [d1 [Frg [ES P]]]]; clear F.
  destruct (foreign_DomRng _ WD _ _ _ Frg) as [AA [BB [CC [DD [EE [FF [GG HH]]]]]]].
  clear DD.
  assert (LOC: local_of nu b1 = Some (b2, d1)).
    apply foreign_in_all in Frg.
    remember (as_inj nu b1) as d.
    destruct d; apply eq_sym in Heqd.
      destruct p. rewrite (AI _ _ _ Heqd) in Frg. inv Frg.
      destruct (joinD_Some _ _ _ _ _ Heqd); try eauto.
        assert (locBlocksTgt nu b2 = false)
           by eapply (extern_DomRng' _ WDnu _ _ _ H2).
        rewrite H3 in H; discriminate.
      apply H2.
    destruct SEP as [SEPa [SEPb SEPc]].
      destruct (SEPa _ _ _ Heqd Frg).
      eelim SEPc; try eassumption.
      eapply (as_inj_DomRng); eassumption.
  destruct (local_DomRng _ WDnu _ _ _ LOC).
  specialize (PB b1); rewrite EE, H2 in PB; simpl in PB.
  destruct (H1 _ _ LOC). contradiction.
  rewrite PB in H4; intuition.
Qed.

Lemma RGTgt_multicorePerm: forall mu Etgt Esrc m2 m2' (WD: SM_wd mu) m1
            (TgtHyp: forall b ofs, Etgt b ofs = true ->
                       (Mem.valid_block m2 b /\
                         (locBlocksTgt mu b = false ->
                           exists b1 delta1, foreign_of mu b1 = Some(b,delta1) /\
                           Esrc b1 (ofs-delta1) = true /\ Mem.perm m1 b1 (ofs-delta1) Max Nonempty)))
            (Unch2: Mem.unchanged_on (fun b z => Etgt b z = false) m2 m2')
            (*(SrcHyp: forall b ofs, Esrc b ofs = true -> vis mu b = true)*)
            nu
         (X1: forall b, locBlocksTgt nu b = true -> locBlocksTgt mu b = false)
         (X2: forall b1 b2 d, foreign_of mu b1 = Some(b2, d) ->
                              locBlocksSrc nu b1 || locBlocksTgt nu b2 = true ->
                              pub_of nu b1 = Some(b2,d)),
            Mem.unchanged_on (local_out_of_reach nu m1) m2 m2'.
Proof. intros.
  eapply mem_unchanged_on_sub; try eassumption; clear Unch2.
  intros. simpl. rename b into b2.
  case_eq (Etgt b2 ofs); intros; trivial.
  destruct (TgtHyp _ _ H0) as [VB2 F]; clear TgtHyp.
  destruct H.
  specialize (X1 _ H).
  destruct (F X1) as [b1 [d1 [Frg [ES P]]]]; clear F.
  destruct (foreign_DomRng _ WD _ _ _ Frg) as [AA [BB [CC [DD [EE [FF [GG HH]]]]]]].
  clear DD.
  (*destruct (SrcHyp _ _ ES); clear SrcHyp.
    rewrite H2 in *. inv CC.
  clear H2.*)
  specialize (X2 _ _ _ Frg). rewrite H in X2.
  rewrite orb_true_r in X2. specialize (X2 (eq_refl _)).
  destruct (H1 b1 d1).
    apply pub_in_local. apply X2.
    contradiction.
  rewrite (pubSrcContra _ _ H2) in X2. inv X2.
Qed.

Lemma RGTgt_multicoreNOEFFECTS: forall mu m2 m2' (WD: SM_wd mu)
            (TgtHyp1: Mem.unchanged_on (fun b2 ofs => extBlocksTgt mu b2 = true /\
                                           ~ exists b1 d, foreign_of mu b1=Some (b2,d)) m2 m2')
            m1 m1'
            (TgtHyp2: forall b ofs, Mem.unchanged_on (fun b' ofs' => b'=b /\ ofs'=ofs) m1 m1' ->
                      forall b2 d, foreign_of mu b = Some(b2,d) ->
                           Mem.unchanged_on (fun b' ofs' => b'=b2 /\ ofs'=ofs+d) m2 m2')
            nu (WDnu: SM_wd nu)
           (FWD1: mem_forward m1 m1')
           (X1: forall b, locBlocksTgt nu b = true ->
                        DomTgt mu b = true /\ locBlocksTgt mu b = false)
           (X2: forall b1 b2 d, foreign_of mu b1 = Some(b2, d) ->
                              locBlocksSrc nu b1 || locBlocksTgt nu b2 = true ->
                              pub_of nu b1 = Some(b2,d))
            (Unch1: Mem.unchanged_on (fun b ofs => locBlocksSrc nu b = true /\
                                           pubBlocksSrc nu b = false) m1 m1')
           (DECIDABILITYAXIOM: forall b2 (E: extBlocksTgt mu b2 = true),
                (exists b1 d, foreign_of mu b1 = Some(b2,d)) \/
                (~ exists b1 d, foreign_of mu b1=Some (b2,d))),
            Mem.unchanged_on (local_out_of_reach nu m1) m2 m2'.
Proof. intros.
split; intros b2; intros.
(*permissions*)
  destruct H.
  destruct (X1 _ H); clear X1.
  assert (extBlocksTgt mu b2 = true).
    unfold DomTgt in H2. rewrite H3 in H2; simpl in H2. assumption.
  destruct (DECIDABILITYAXIOM _ H4); clear DECIDABILITYAXIOM.
    destruct H5 as [b1 [dd FRGN]].
    specialize (X2 _ _ _ FRGN). rewrite H in X2.
    assert (local_of nu b1 = Some(b2,dd)). apply pub_in_local. apply X2; intuition.
    eapply TgtHyp2; clear TgtHyp2; try eassumption.
    Focus 2. split. trivial. instantiate (1:=ofs-dd). omega.
    destruct (H1 _ _ H5); clear H1.
      eapply forward_unchanged_on; assumption.
    eapply mem_unchanged_on_sub; try eassumption.
      intros. destruct H1; subst. split; trivial.
      eapply (local_DomRng _ WDnu _ _ _ H5).
  eapply TgtHyp1. split; trivial. assumption.
(*Values - same proof*)
  destruct H.
  destruct (X1 _ H); clear X1.
  assert (extBlocksTgt mu b2 = true).
    unfold DomTgt in H2. rewrite H3 in H2; simpl in H2. assumption.
  destruct (DECIDABILITYAXIOM _ H4); clear DECIDABILITYAXIOM.
    destruct H5 as [b1 [dd FRGN]].
    specialize (X2 _ _ _ FRGN). rewrite H in X2.
    assert (local_of nu b1 = Some(b2,dd)). apply pub_in_local. apply X2; intuition.
    eapply TgtHyp2; clear TgtHyp2; try eassumption.
    Focus 2. split. trivial. instantiate (1:=ofs-dd). omega.
    destruct (H1 _ _ H5); clear H1.
      eapply forward_unchanged_on; assumption.
    eapply mem_unchanged_on_sub; try eassumption.
      intros. destruct H1; subst. split; trivial.
      eapply (local_DomRng _ WDnu _ _ _ H5).
  eapply TgtHyp1. split; trivial. assumption.
Qed.

Record LinkInv (mu0 mu: SM_Injection) :=
  { LinkInv_WD0: SM_wd mu0;
    LinkInv_WD:  SM_wd mu;
    LinkInv_DomSrc: forall b, DomSrc mu0 b = true -> DomSrc mu b = true;
    LinkInv_DomTgt: forall b, DomTgt mu0 b = true -> DomTgt mu b = true;
    LinkInv_Restrict: restrict (as_inj mu) (DomSrc mu0) = as_inj mu0;
    LinkInv_Sep: forall b1 b2 d, as_inj mu0 b1 = None -> as_inj mu b1 = Some(b2,d) ->
                       (DomSrc mu0 b1 = false /\ DomTgt mu0 b2 = false) }.

Lemma LinkInv_sound: forall mu0 mu (LI : LinkInv mu0 mu)
         nu (NU: nu = reestablish mu0 mu),
      SM_wd nu /\ DomSrc nu = DomSrc mu /\ DomTgt nu = DomTgt mu /\
      extern_incr mu0 nu /\ as_inj nu = as_inj mu /\
      (forall m1 m2, sm_inject_separated mu0 mu m1 m2 ->
              sm_inject_separated mu0 nu m1 m2) /\
      (forall m1 m2, sm_valid mu m1 m2 ->
              sm_valid (reestablish mu0 mu) m1 m2) /\
      (forall mu', SM_wd mu' -> intern_incr mu mu' ->
                   extern_incr mu0 (reestablish mu0 mu')).
Proof. intros. subst.
assert (LocSrc: forall b, locBlocksSrc mu0 b = true -> DomSrc mu b = true).
   intros. eapply (LinkInv_DomSrc _ _ LI); unfold DomSrc; intuition.
assert (ExtSrc: forall b, extBlocksSrc mu0 b = true -> DomSrc mu b = true).
   intros. eapply (LinkInv_DomSrc _ _ LI); unfold DomSrc; intuition.
assert (LocTgt: forall b, locBlocksTgt mu0 b = true -> DomTgt mu b = true).
   intros. eapply (LinkInv_DomTgt _ _ LI); unfold DomTgt; intuition.
assert (ExtTgt: forall b, extBlocksTgt mu0 b = true -> DomTgt mu b = true).
   intros. eapply (LinkInv_DomTgt _ _ LI); unfold DomTgt; intuition.
assert (DS:= reestablish_DomSrc _ _ LocSrc).
assert (DT:= reestablish_DomTgt _ _ LocTgt).
intuition.
  eapply reestablish_wd; try eassumption; eapply LI.
  eapply reestablish_extern_incr; eassumption.
  eapply reestablish_as_inj; eassumption.
  eapply reestablish_sm_injsep; try eassumption.
  eapply reestablish_sm_valid; try eassumption.
  eapply (reestablish_internstep mu0 mu mu'); try eassumption.
Qed.

Lemma atExternal_Protected: forall mu m1
         (MatchProtected: forall b, REACH m1 (extBlocksSrc mu) b = true ->
                        locBlocksSrc mu b = true ->
                        REACH m1 (sharedSrc mu) b = true)
        vals1 vals2
        (ValInjMu: Forall2 (val_inject (as_inj mu)) vals1 vals2)
        pubSrc' (pubSrcHyp: pubSrc' = fun b => andb (locBlocksSrc mu b)
                                                    (REACH m1 (exportedSrc mu vals1) b))

        pubTgt'
        nu (NuHyp: nu = replace_locals mu pubSrc' pubTgt'),
    forall b, REACH m1 (extBlocksSrc nu) b = true ->
                        locBlocksSrc nu b = true ->
                        pubBlocksSrc nu b = true.
Proof. intros. subst.
  rewrite replace_locals_pubBlocksSrc.
  rewrite replace_locals_locBlocksSrc in H0.
  rewrite replace_locals_extBlocksSrc in H.
  rewrite H0; simpl.
  specialize (MatchProtected _ H H0).
  eapply REACH_mono; try eapply MatchProtected.
  unfold exportedSrc. intuition.
Qed.

author: PrincetonUniversity

repo: compcomp