From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Extras.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import InterContractCommunication.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Examples.Dexter2 Require Import Dexter2FA12. Import DEX2LQT.
From Coq Require Import ZArith_base.
From Coq Require Import Bool.
From Coq Require Import List. Import ListNotations.
From Coq Require Import Lia.

Section Theories.
  Context `{ChainBase}.
  Open Scope N_scope.

  Lemma contract_not_payable : forall prev_state new_state chain ctx msg new_acts,
    receive_lqt chain ctx prev_state msg = Ok (new_state, new_acts) ->
      ((ctx_amount ctx) <= 0)%Z.
  Proof.
    intros * receive_some.
    unfold receive_lqt, throwIf in receive_some; cbn in receive_some.
    destruct (0 <? _)%Z eqn:amount in receive_some.
    - (* case: ctx_amount > 0 *)
      congruence.
    - (* case: ctx_amount <= 0 *)
      now rewrite Z.ltb_ge in amount.
  Qed.

  Lemma contract_not_payable' : forall prev_state chain ctx msg,
    (0 < (ctx_amount ctx))%Z ->
      receive_lqt chain ctx prev_state msg = Err default_error.
  Proof.
    intros * ctx_amount_positive.
    unfold receive_lqt,throwIf; cbn.
    destruct (0 <? _)%Z eqn:amount.
    - (* case: ctx_amount > 0 *)
      reflexivity.
    - (* case: ctx_amount <= 0 *)
      now apply Z.ltb_ge in amount.
  Qed.


  (* Admin cannot be changed *)
  Lemma admin_constant : forall prev_state new_state chain ctx new_acts msg,
    receive_lqt chain ctx prev_state msg = Ok (new_state, new_acts) ->
      admin prev_state = admin new_state.
  Proof.
    intros * receive_some.
    destruct_message;
      now contract_simpl.
  Qed.

  (* Default entrypoint should never succeed *)
  Lemma default_entrypoint_none : forall prev_state chain ctx,
    receive_lqt chain ctx prev_state None = Err default_error.
  Proof.
    intros *.
    contract_simpl.
    destruct_match eqn:e;
      destruct_throw_if e.
  Qed.

  Definition transfer_balance_update_correct old_state new_state from to amount :=
    let get_balance addr state := with_default 0 (FMap.find addr state.(tokens)) in
    let from_balance_before := get_balance from old_state in
    let to_balance_before := get_balance to old_state in
    let from_balance_after := get_balance from new_state in
    let to_balance_after := get_balance to new_state in
    (* If the transfer is a self-transfer, balances should remain unchained *)
    if address_eqb from to
    then
      (from_balance_before =? from_balance_after) &&
      (to_balance_before =? to_balance_after)
    else
      (from_balance_before =? from_balance_after + amount) &&
      (to_balance_before + amount =? to_balance_after).

  Lemma try_transfer_balance_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
    transfer_balance_update_correct prev_state new_state param.(from) param.(to) param.(value) = true.
  Proof.
    intros * receive_some.
    contract_simpl.
    match goal with
      [ H : with_default 0 _ <? _ = false |- _ ] => rename H into enough_balance
    end.
    rewrite N.ltb_ge in enough_balance.
    unfold transfer_balance_update_correct.
    cbn.
    destruct_match eqn:from_to_eqb.
    - (* from = to *)
      destruct (address_eqb_spec param.(from) param.(to)) as [<-|]; auto.
      rewrite !FMap.map_update_idemp.
      rewrite !FMap.find_update_eq with (map := prev_state.(tokens)).
      destruct (FMap.find (from param) _) eqn:from_prev; cbn in *.
      + now apply maybe_sub_add in enough_balance as [[-> ->] | ->]; rewrite N.eqb_refl.
      + rewrite N.add_0_l.
        apply N.le_0_r in enough_balance.
        now rewrite enough_balance.
    - (* from <> to *)
      destruct (address_eqb_spec param.(from) param.(to)) as [| from_to_eq]; auto.
      rewrite !FMap.find_update_ne with (map := prev_state.(tokens)) by auto.
      rewrite !FMap.find_update_ne by auto.
      rewrite !FMap.find_update_eq.
      destruct (FMap.find (from param) _) eqn:from_prev; cbn;
        [| apply N.le_0_r in enough_balance; rewrite enough_balance];
      destruct (FMap.find (to param) _) eqn:to_prev; cbn;
      rewrite ?N.add_0_l, ?N.add_0_r, ?N.sub_add, ?N.eqb_refl by auto;
      rewrite andb_true_iff, ?N.eqb_eq;
      cbn in enough_balance.
      * specialize (maybe_cases (n - value param)) as [[-> ?H] | [-> _]];
        specialize (maybe_cases (n0 + value param)) as [[-> ?H] | [-> _]];
        cbn; lia.
      * specialize (maybe_cases (n - value param)) as [[-> ?H] | [-> _]];
        specialize (maybe_cases (value param)) as [[-> ?H] | [-> _]];
        cbn; lia.
      * now specialize (maybe_cases n) as [[-> ?H] | [-> _]].
      * auto.
  Qed.

  Definition transfer_allowances_update_correct old_state new_state sender from amount :=
    let get_allowance addr1 addr2 state := with_default 0 (FMap.find (addr1, addr2) state.(allowances)) in
    let allowance_before := get_allowance from sender old_state in
    let allowance_after := get_allowance from sender new_state in
    (* If from and sender is equal, allowances should remain unchained *)
    if address_eqb sender from
    then
      (allowance_before =? allowance_after)
    else
      (allowance_before =? allowance_after + amount).

  Lemma try_transfer_allowance_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
    transfer_allowances_update_correct prev_state new_state ctx.(ctx_from) param.(from) param.(value) = true.
  Proof.
    intros * receive_some.
    contract_simpl.
    unfold transfer_allowances_update_correct.
    cbn.
    destruct_match eqn:sender_from_eqb.
    - (* sender = from *)
      match goal with
      [ H : Ok (allowances _) = Ok _ |- _ ] => rename H into allowances_eq
      end.
      inversion_clear allowances_eq.
      now rewrite N.eqb_refl.
    - (* sender <> from *)
      contract_simpl.
      match goal with
      [ H : with_default 0 (FMap.find _ (allowances _)) <? _ = false |- _ ] => rename H into enough_allowance
      end.
      rewrite N.ltb_ge in enough_allowance.
      rewrite FMap.find_update_eq.
      destruct (FMap.find (from param, ctx_from ctx) (allowances prev_state)) eqn:from_prev; cbn.
      + unfold maybe.
        destruct (n - value param =? 0) eqn:n_eq_value; cbn.
        * apply N.eqb_eq in n_eq_value.
          rewrite N.sub_0_le in n_eq_value.
          erewrite (N.le_antisymm n _) by eassumption.
          now rewrite !N.eqb_refl.
        * now rewrite N.sub_add, N.eqb_refl.
      + apply N.le_0_r in enough_allowance.
        now rewrite enough_allowance.
  Qed.

  Lemma try_transfer_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      new_acts = [].
  Proof.
    intros * receive_some.
    contract_simpl.
  Qed.

  Lemma try_transfer_preserves_total_supply : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      total_supply prev_state = total_supply new_state.
  Proof.
    intros * receive_some.
    contract_simpl.
  Qed.

  Lemma try_transfer_preserves_other_balances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      forall account, account <> param.(from) -> account <> param.(to) ->
        FMap.find account (tokens prev_state) = FMap.find account (tokens new_state).
  Proof.
    intros * receive_some account account_not_from account_not_to.
    contract_simpl.
    cbn.
    now rewrite !FMap.find_update_ne.
  Qed.

  Lemma try_transfer_preserves_other_allowances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      forall allowance_key, allowance_key <> (param.(from), ctx.(ctx_from)) ->
        FMap.find allowance_key (allowances prev_state) = FMap.find allowance_key (allowances new_state).
  Proof.
    intros * receive_some account allowance_key_ne.
    contract_simpl.
    cbn.
    match goal with
      [ H : _ = Ok _ |- _ ] => rename H into allowance_eq
    end.
    destruct_address_eq.
    - (* from = sender *)
      now inversion_clear allowance_eq.
    - (* from <> sender *)
      destruct_match in allowance_eq;
        inversion_clear allowance_eq.
      now rewrite !FMap.find_update_ne.
  Qed.

  Lemma try_transfer_remove_empty_allowances : forall prev_state new_state chain ctx new_acts param,
    (forall n, FMap.find (param.(from), ctx.(ctx_from)) (allowances prev_state) = Some n -> n > 0) ->
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      forall n, FMap.find (param.(from), ctx.(ctx_from)) (allowances new_state) = Some n -> n > 0.
  Proof.
    intros * IH receive_some *.
    contract_simpl.
    destruct_match in *.
    - now contract_simpl.
    - contract_simpl.
      rewrite !FMap.find_update_eq.
      now edestruct maybe_cases as [[-> ?H] | [-> ?H]].
  Qed.

  Lemma try_transfer_remove_empty_balances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_transfer param)) = Ok (new_state, new_acts) ->
      forall n,
      (FMap.find param.(from) (tokens new_state) = Some n -> n > 0) /\
      (FMap.find param.(to) (tokens new_state) = Some n -> n > 0).
  Proof.
    intros * receive_some *.
    contract_simpl.
    rewrite N.ltb_ge in *.
    destruct (address_eqb_spec param.(from) param.(to)) as [<-|]; auto.
    - rewrite !FMap.find_update_eq.
      now edestruct maybe_cases as [[-> ?H] | [-> ?H]].
    - rewrite !FMap.find_update_ne by auto.
      rewrite !FMap.find_update_eq.
      rewrite !FMap.find_update_ne with (map := prev_state.(tokens)) by auto.
      edestruct maybe_cases as [[-> ?H] | [-> ?H]];
      now edestruct maybe_cases as [[-> ?H] | [-> ?H]].
  Qed.

  Lemma try_transfer_is_some : forall state chain ctx param,
    (ctx_amount ctx <= 0)%Z /\
    param.(value) <= with_default 0 (FMap.find param.(from) (tokens state)) /\
    (param.(from) <> ctx.(ctx_from) ->
      param.(value) <= with_default 0 (FMap.find (param.(from), ctx.(ctx_from)) (allowances state)))
      <-> exists new_state new_acts, receive_lqt chain ctx state (Some (msg_transfer param)) = Ok (new_state, new_acts).
  Proof.
    split.
    - intros (amount_zero & enough_balance & enough_allowance).
      apply Z.ltb_ge in amount_zero.
      cbn.
      rewrite amount_zero; cbn.
      destruct_match eqn:receive_some;
      destruct_match eqn:allowances_eq in receive_some;
      destruct_match eqn:sender_from_eqb in allowances_eq; try congruence;
      try destruct_match eqn:enough_allowance_check in allowances_eq; try congruence;
      try destruct_match eqn:new_balance in receive_some;
      try destruct_match eqn:enough_balance_check in new_balance; try congruence.
      + (* case no contradictions *)
        now inversion_clear allowances_eq.
      + (* case: no contradictions *)
        now inversion_clear allowances_eq.
      + (* enough balances contradiction *)
        contract_simpl.
        apply N.ltb_lt in enough_balance_check.
        now apply N.le_ngt in enough_balance.
      + (* enough balances contradiction *)
        contract_simpl.
        apply N.ltb_lt in enough_balance_check.
        now apply N.le_ngt in enough_balance.
      + (* enough allowance contradiction *)
        contract_simpl.
        apply N.ltb_lt in enough_allowance_check.
        destruct (address_eqb_spec ctx.(ctx_from) param.(from)) as [| sender_from_ne]; try discriminate.
        now apply not_eq_sym, enough_allowance, N.le_ngt in sender_from_ne.
    - intros (new_state & new_acts & receive_some).
      contract_simpl.
      rewrite Z.ltb_ge in *.
      split; try assumption.
      rewrite N.ltb_ge in *.
      destruct_match eqn:sender_from_eqb in *.
        destruct (address_eqb_spec ctx.(ctx_from) param.(from)) as
          [send_from_eq | sender_from_ne]; contract_simpl; try discriminate.
      + (* sender = from *)
        now split.
      + (* sender <> from *)
        destruct_match eqn:enough_allowance in *; try congruence.
        contract_simpl.
        now apply N.ltb_ge in enough_allowance.
  Qed.

  Lemma try_approve_allowance_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      FMap.find (ctx.(ctx_from), param.(spender)) (allowances new_state) = maybe param.(value_).
  Proof.
    intros * receive_some.
    contract_simpl.
    cbn.
    now rewrite !FMap.find_update_eq.
  Qed.

  Lemma try_approve_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      new_acts = [].
  Proof.
    intros * receive_some.
    contract_simpl.
  Qed.

  Lemma try_approve_preserves_other_allowances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      forall allowance_key, allowance_key <> (ctx.(ctx_from), param.(spender)) ->
        FMap.find allowance_key (allowances prev_state) = FMap.find allowance_key (allowances new_state).
  Proof.
    intros * receive_some allowance_key allowance_key_ne.
    contract_simpl.
    cbn.
    now rewrite FMap.find_update_ne.
  Qed.

  Lemma try_approve_preserves_total_supply : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      total_supply prev_state = total_supply new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_approve_preserves_balances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      tokens prev_state = tokens new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_approve_remove_empty_allowances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_approve param)) = Ok (new_state, new_acts) ->
      forall n, FMap.find (ctx.(ctx_from), param.(spender)) (allowances new_state) = Some n -> n > 0.
  Proof.
    intros * IH receive_some *.
    contract_simpl.
    cbn.
    rewrite FMap.find_update_eq.
    now edestruct maybe_cases as [[-> ?H] | [-> ?H]].
  Qed.

  Lemma try_approve_is_some : forall state chain ctx param,
    (ctx_amount ctx <= 0)%Z /\
    (with_default 0 (FMap.find (ctx.(ctx_from), param.(spender)) (allowances state)) = 0 \/ param.(value_) = 0)
      <-> exists new_state new_acts, receive_lqt chain ctx state (Some (msg_approve param)) = Ok (new_state, new_acts).
  Proof.
    split;
      intros;
      destruct_hyps;
      contract_simpl;
      propify;
      try easy.
    destruct_match eqn:H4 in H3; try congruence.
    destruct_throw_if H4.
    now propify.
  Qed.

  Lemma try_mint_or_burn_balance_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
      (Z.of_N (with_default 0%N (FMap.find param.(target) (tokens prev_state))) + param.(quantity) =
      Z.of_N (with_default 0%N (FMap.find param.(target) (tokens new_state))))%Z.
  Proof.
    intros * receive_some.
    contract_simpl.
    rewrite Z.ltb_ge in *.
    cbn.
    rewrite FMap.find_update_eq.
    unfold maybe.
    unfold FMap.find in *. (* NOTE: after using AddressMap, unification fails sometime, unless we unfold FMap.find and other definitions. *)
    destruct (Z.to_N (Z.of_N (with_default 0 _) + quantity param) =? 0) eqn:eq_zero; cbn.
    - apply N.eqb_eq in eq_zero. unfold FMap.find in *.
      lia.
    - rewrite <- Z2N.id by lia.
      lia.
  Qed.

  Lemma try_mint_or_burn_total_supply_correct : forall prev_state new_state chain ctx new_acts param,
    with_default 0 (FMap.find param.(target) (tokens prev_state)) <= total_supply prev_state ->
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
      (Z.of_N prev_state.(total_supply) + param.(quantity) =
      Z.of_N new_state.(total_supply))%Z.
  Proof.
    intros * balance_le_total_supply receive_some.
    contract_simpl.
    rewrite Z.ltb_ge in *.
    cbn.
    rewrite N2Z.inj_abs_N, Z.abs_eq; auto.
    unfold FMap.find in *; lia.
  Qed.

  Lemma try_mint_or_burn_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
      new_acts = [].
  Proof.
    intros.
    contract_simpl.
  Qed.

  Lemma try_mint_or_burn_preserves_other_balances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
      forall account, account <> param.(target) ->
        FMap.find account (tokens prev_state) = FMap.find account (tokens new_state).
  Proof.
    intros * receive_some account account_not_target.
    contract_simpl.
    cbn.
    now rewrite FMap.find_update_ne.
  Qed.

  Lemma try_mint_or_burn_preserves_allowances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
        allowances prev_state = allowances new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_mint_or_burn_remove_empty_balances : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts) ->
      forall n, FMap.find param.(target) (tokens new_state) = Some n -> n > 0.
  Proof.
    intros * receive_some *.
    contract_simpl.
    rewrite Z.ltb_ge in *.
    cbn.
    rewrite FMap.find_update_eq.
    now edestruct maybe_cases as [[-> ?H] | [-> ?H]].
  Qed.

  Lemma try_mint_or_burn_is_some : forall state chain ctx param,
    (ctx_amount ctx <= 0)%Z /\
    ctx.(ctx_from) = state.(admin) /\
    (0 <= Z.of_N (with_default 0%N (FMap.find param.(target) (tokens state))) + param.(quantity))%Z
      <-> exists new_state new_acts, receive_lqt chain ctx state (Some (msg_mint_or_burn param)) = Ok (new_state, new_acts).
  Proof.
    split;
      intros;
      destruct_hyps;
      contract_simpl;
      propify;
      try easy;
      try now destruct_address_eq.
    destruct_match eqn:H5 in H4; try congruence.
    destruct_match eqn:H6 in H4; try congruence.
    destruct_throw_if H5.
    destruct_throw_if H6.
    now propify.
    now destruct_address_eq.
  Qed.

  Lemma try_get_allowance_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_allowance param)) = Ok (new_state, new_acts) ->
      new_acts = [
        act_call param.(allowance_callback) 0%Z (serialize
          (receive_allowance (with_default 0 (FMap.find param.(request) (allowances prev_state)))))
      ].
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_allowance_preserves_state : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_allowance param)) = Ok (new_state, new_acts) ->
      prev_state = new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_allowance_is_some : forall prev_state chain ctx param,
    (ctx_amount ctx <= 0)%Z <->
    exists new_state new_acts, receive_lqt chain ctx prev_state (Some (msg_get_allowance param)) = Ok (new_state, new_acts).
  Proof.
    split;
      intros;
      destruct_hyps;
      contract_simpl;
      now propify.
  Qed.

  Lemma try_get_balance_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_balance param)) = Ok (new_state, new_acts) ->
      new_acts = [
        act_call param.(balance_callback) 0%Z (serialize
          (receive_balance_of (with_default 0 (FMap.find param.(owner_) (tokens prev_state)))))
      ].
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_balance_preserves_state : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_balance param)) = Ok (new_state, new_acts) ->
      prev_state = new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_balance_is_some : forall prev_state chain ctx param,
    (ctx_amount ctx <= 0)%Z <->
    exists new_state new_acts, receive_lqt chain ctx prev_state (Some (msg_get_balance param)) = Ok (new_state, new_acts).
  Proof.
    split;
      intros;
      destruct_hyps;
      contract_simpl;
      now propify.
  Qed.

  Lemma try_get_total_supply_new_acts_correct : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_total_supply param)) = Ok (new_state, new_acts) ->
      new_acts = [
        act_call param.(supply_callback) 0%Z (serialize
          (receive_total_supply prev_state.(total_supply)))
      ].
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_total_supply_preserves_state : forall prev_state new_state chain ctx new_acts param,
    receive_lqt chain ctx prev_state (Some (msg_get_total_supply param)) = Ok (new_state, new_acts) ->
      prev_state = new_state.
  Proof.
    intros * receive_some.
    now contract_simpl.
  Qed.

  Lemma try_get_total_supply_is_some : forall prev_state chain ctx param,
    (ctx_amount ctx <= 0)%Z <->
    exists new_state new_acts, receive_lqt chain ctx prev_state (Some (msg_get_total_supply param)) = Ok (new_state, new_acts).
  Proof.
    split;
      intros;
      destruct_hyps;
      contract_simpl;
      now propify.
  Qed.

  Lemma init_balances_correct : forall chain ctx setup state,
    init_lqt chain ctx setup = Ok state ->
      state.(tokens) = FMap.add setup.(lqt_provider) setup.(initial_pool) FMap.empty.
  Proof.
    intros * init_some.
    now inversion init_some.
  Qed.

  Lemma init_allowances_correct : forall chain ctx setup state,
    init_lqt chain ctx setup = Ok state ->
      state.(allowances) = FMap.empty.
  Proof.
    intros * init_some.
    now inversion init_some.
  Qed.

  Lemma init_admin_correct : forall chain ctx setup state,
    init_lqt chain ctx setup = Ok state ->
      state.(admin) = setup.(admin_).
  Proof.
    intros * init_some.
    now inversion init_some.
  Qed.

  Lemma init_total_supply_correct : forall chain ctx setup state,
    init_lqt chain ctx setup = Ok state ->
      state.(total_supply) = setup.(initial_pool).
  Proof.
    intros * init_some.
    now inversion init_some.
  Qed.

  Lemma init_is_some : forall chain ctx setup,
    exists state, init_lqt chain ctx setup = state.
  Proof.
    intros.
    eauto.
  Qed.

  Lemma only_getter_self_calls bstate caddr :
    reachable bstate ->
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    Forall (fun act_body =>
      match act_body with
      | act_transfer to _ => False
      | act_call to _ msg => to = caddr ->
          (exists n, msg = serialize (receive_allowance n)) \/
          (exists n, msg = serialize (receive_balance_of n)) \/
          (exists n, msg = serialize (receive_total_supply n))
      | _ => False
      end) (outgoing_acts bstate caddr).
  Proof.
    contract_induction; intros; auto.
    - now inversion IH.
    - apply Forall_app; split; auto.
      clear IH. simpl in *.
      destruct msg.
      + destruct m;
          try_solve_acts_correct.
      + contract_simpl.
    - inversion_clear IH as [|? ? head_not_me tail_not_me].
      destruct head;
        try contradiction.
      destruct action_facts as (? & ? & ? & ?).
      subst.
      destruct head_not_me as [[] | [[] | []]]; auto;
        subst;
        now contract_simpl.
    - now rewrite <- perm.
    - solve_facts.
  Qed.

  Lemma no_self_calls : forall bstate origin from_addr to_addr amount msg acts ctx prev_state new_state resp_acts,
    reachable bstate ->
    env_contracts bstate to_addr = Some (contract : WeakContract) ->
    chain_state_queue bstate =
    {| act_origin := origin;
      act_from := from_addr;
      act_body :=
        match msg with
        | Some msg => act_call to_addr amount msg
        | None => act_transfer to_addr amount
      end |} :: acts ->
    wc_receive contract bstate ctx prev_state msg = Ok (new_state, resp_acts) ->
    from_addr <> to_addr.
  Proof.
    intros * reach deployed queue receive_some.
    apply only_getter_self_calls in deployed as no_self_calls; auto.
    unfold outgoing_acts in no_self_calls.
    rewrite queue in no_self_calls.
    cbn in no_self_calls.
    destruct_address_eq; auto.
    inversion_clear no_self_calls as [|? ? hd _].
    destruct msg; auto.
    destruct hd as [[] | [[] | []]];
      auto; subst;
      eapply wc_receive_strong in receive_some as (_ & ? & _ & _ & msg_correct & _);
      now destruct_match in msg_correct.
  Qed.

  Lemma new_acts_amount_zero : forall prev_state chain ctx msg new_state new_acts,
    receive_lqt chain ctx prev_state msg = Ok (new_state, new_acts) ->
      sumZ (fun act => act_body_amount act) new_acts = 0%Z.
  Proof.
    intros * receive_some.
    destruct msg.
    - destruct m; try_solve_acts_correct.
    - contract_simpl.
  Qed.

  Lemma outgoing_acts_amount_zero : forall bstate caddr,
    reachable bstate ->
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    Forall (fun act => act_body_amount act = 0%Z) (outgoing_acts bstate caddr).
  Proof.
    intros * reach deployed.
    apply (lift_outgoing_acts_prop contract); auto.
    intros * receive_some. simpl in *.
    destruct msg.
    - destruct m; try_solve_acts_correct.
    - contract_simpl.
  Qed.

  Lemma outgoing_acts_are_calls : forall bstate caddr,
    reachable bstate ->
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    Forall (fun act_body =>
      match act_body with
      | act_call _ _ _ => True
      | _ => False
      end) (outgoing_acts bstate caddr).
  Proof.
    intros * reach deployed.
    apply (lift_outgoing_acts_prop contract); auto.
    intros * receive_some; simpl in *.
    destruct msg.
    - destruct m; try_solve_acts_correct.
    - contract_simpl.
  Qed.

  (* Contract balance should never change and thus always be equal to the deploy amount *)
  Lemma contract_balance_bound' : forall bstate caddr (trace : ChainTrace empty_state bstate),
    let effective_balance := (env_account_balances bstate caddr - (sumZ (fun act => act_body_amount act) (outgoing_acts bstate caddr)))%Z in
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    exists deploy_info,
      deployment_info Setup trace caddr = Some deploy_info
      /\ effective_balance = deploy_info.(deployment_amount).
  Proof.
    intros.
    subst effective_balance.
    contract_induction; intros; auto.
    - cbn.
      lia.
    - cbn in IH.
      lia.
    - instantiate (CallFacts := fun _ ctx _ _ _ =>
        (0 <= ctx_amount ctx)%Z /\ ctx_from ctx <> ctx_contract_address ctx).
      destruct facts as (ctx_amount_positive & _).
      simpl in *.
      apply contract_not_payable in receive_some as not_payable.
      apply new_acts_amount_zero in receive_some as amount_zero_new_acts.
      apply Z.le_antisymm in ctx_amount_positive; auto.
      rewrite ctx_amount_positive, Z.sub_0_r in IH.
      now rewrite sumZ_app, amount_zero_new_acts, Z.add_0_l.
    - now destruct facts.
    - now erewrite sumZ_permutation in IH by eauto.
    - solve_facts.
      split.
      + now apply Z.ge_le.
      + rewrite deployed in *.
        match goal with
        | H : Some ?x = Some _ |- _ => inversion H; subst x; clear H
        end.
        eapply no_self_calls; eauto.
        now constructor.
  Qed.

  Lemma contract_balance_bound : forall bstate caddr (trace : ChainTrace empty_state bstate),
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    exists deploy_info,
      deployment_info Setup trace caddr = Some deploy_info
      /\ env_account_balances bstate caddr = deploy_info.(deployment_amount).
  Proof.
    intros * deployed.
    edestruct contract_balance_bound' as (dep_info & deployment_info_eq & balance_bound); eauto.
    eexists.
    rewrite deployment_info_eq.
    split; eauto.
    rewrite <- balance_bound.
    rewrite Zminus_0_l_reverse, Z.sub_cancel_l at 1.
    apply outgoing_acts_amount_zero in deployed as act_amount_zero;
      try now constructor.
    clear balance_bound deployment_info_eq dep_info trace deployed.
    induction (outgoing_acts bstate caddr).
    - reflexivity.
    - cbn.
      apply list.Forall_cons in act_amount_zero as (act_amount_zero & acts_amount_zero).
      rewrite act_amount_zero, Z.add_0_l.
      now apply IHl.
  Qed.

  Definition sum_balances state :=
    sumN (fun '(k, v) => v) (FMap.elements (tokens state)).

  Lemma balance_le_sum_balances : forall addr state,
    with_default 0 (FMap.find addr (tokens state)) <= sum_balances state.
  Proof.
    intros.
    destruct FMap.find eqn:balance.
    - eapply FMap.In_elements, sumN_in_le in balance.
      eapply N.le_trans; cycle 1; eauto.
    - apply N.le_0_l.
  Qed.

  Ltac FMap_simpl_step :=
    match goal with
      | |- context [ FMap.find ?x (FMap.add ?x _ _) ] => setoid_rewrite FMap.find_add
      | H : FMap.find ?t ?m = Some _ |- FMap.find ?t ?m = Some _ => cbn; rewrite H; f_equal; lia
      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
      | H : FMap.find ?x _ = Some _ |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add_existing; eauto
      | |- context [ FMap.add ?x _ (FMap.add ?x _ _) ] => setoid_rewrite FMap.add_add
      | H : FMap.find ?x _ = None |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add; eauto
      | |- context [ FMap.remove ?x (FMap.add ?x _ _) ] => rewrite fin_maps.delete_insert_delete
      | |- context [ FMap.find ?x (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter
      | H : ?x' <> ?x |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne; auto
      | H : ?x <> ?x' |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne
      | H : context [ AddressMap.find _ _ ] |- _ => rewrite AddressMap_find_convertible in H
      | H : context [ AddressMap.add _ _ _ ] |- _ => rewrite AddressMap_add_convertible in H
      | |- context [ AddressMap.find _ _ ] => rewrite AddressMap_find_convertible
      | |- context [ AddressMap.add _ _ _ ] => rewrite AddressMap_add_convertible
      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.remove ?y _) ] => rewrite FMap.find_remove_ne; eauto
      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.remove ?y _) ] => rewrite FMap.find_remove_ne; eauto
    end.

  Tactic Notation "FMap_simpl" := repeat (FMap_simpl_step; cbn).

  Lemma sum_balances_eq_total_supply : forall bstate caddr,
    reachable bstate ->
    env_contracts bstate caddr = Some (contract : WeakContract) ->
    exists cstate,
      contract_state bstate caddr = Some cstate
      /\ total_supply cstate = sum_balances cstate.
  Proof.
    intros * reach deployed.
    apply (lift_contract_state_prop contract);
      intros *; simpl in *; auto; clear reach deployed bstate caddr.
    - intros init_some.
      unfold sum_balances. cbn in *.
      erewrite init_total_supply_correct, init_balances_correct; eauto.
      rewrite FMap.elements_add, FMap.elements_empty by auto.
      now cbn.
    - intros IH receive_some.
      destruct msg. destruct m.
      + erewrite <- try_transfer_preserves_total_supply; eauto.
        rename t into param.
        unfold sum_balances.
        contract_simpl.
        cbn.
        rewrite N.ltb_ge in *.
        destruct (address_eqb_spec param.(from) param.(to)) as
          [<-| from_to_ne];
          [rewrite FMap.find_update_eq | rewrite FMap.find_update_ne by auto];
          destruct (FMap.find (from param) _) eqn:from_balance;
          destruct (FMap.find (to param) (tokens cstate)) eqn:to_balance;
          destruct param; cbn in *.
          * rewrite FMap.map_update_idemp.
            unfold FMap.update.
            apply maybe_sub_add in H1 as [[-> ->] | ->].
            -- rewrite <- N.add_0_r.
               change 0 with ((fun '(_, v) => v) (from, 0)).
               rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
            -- FMap_simpl_step.
               rewrite fin_maps.map_to_list_delete; auto.
          * rewrite FMap.map_update_idemp.
            unfold FMap.update.
            apply maybe_sub_add in H1 as [[-> ->] | ->].
            -- rewrite <- N.add_0_r.
               change 0 with ((fun '(_, v) => v) (from, 0)).
               rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
            -- FMap_simpl_step.
               rewrite fin_maps.map_to_list_delete; auto.
          * rewrite FMap.map_update_idemp.
            unfold FMap.update.
            apply maybe_sub_add in H1 as [[-> _] | ->].
            -- now rewrite fin_maps.delete_notin.
            -- FMap_simpl_step.
          * rewrite FMap.map_update_idemp.
            unfold FMap.update.
            apply maybe_sub_add in H1 as [[-> _] | ->].
            -- now rewrite fin_maps.delete_notin.
            -- FMap_simpl_step.
          * unfold FMap.update.
            edestruct maybe_cases as [[-> ?H] | [-> _]].
            -- apply N.eq_add_0 in H3 as []; subst.
               edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  rewrite <- N.add_0_r.
                  change 0 with ((fun '(_, v) => v) (to, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  rewrite <- N.add_0_r.
                  change 0 with ((fun '(_, v) => v) (from, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
              --- rewrite N.sub_0_r.
                  rewrite <- N.add_0_r.
                  change 0 with ((fun '(_, v) => v) (to, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  FMap_simpl_step.
                  rewrite fin_maps.map_to_list_delete; auto.
            -- edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite (sumN_split _ (to, n) (to, n0)) by lia.
                  rewrite <- sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  change n with ((fun '(_, v) => v) (from, n)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
              --- FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite (sumN_split _ (to, value) (to, n0)) by lia.
                  rewrite <- sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  FMap_simpl_step.
                  change value with ((fun '(_, v) => v) (from, value)).
                  rewrite sumN_inv.
                  rewrite <- (sumN_split _ _ _ (from, n)) by lia.
                  rewrite fin_maps.map_to_list_delete; auto.
          * rewrite N.add_0_l.
            unfold FMap.update.
            edestruct maybe_cases as [[-> ->] | [-> _]].
            -- edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  rewrite <- N.add_0_r.
                  rewrite fin_maps.delete_notin.
                  2: FMap_simpl_step.
                  change 0 with ((fun '(_, v) => v) (from, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
              --- rewrite N.sub_0_r.
                  rewrite fin_maps.delete_notin.
                  2: FMap_simpl_step.
                  FMap_simpl_step.
                  rewrite fin_maps.map_to_list_delete; auto.
            -- edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite <- sumN_inv.
                  change n with ((fun '(_, v) => v) (from, n)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete; auto.
              --- FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite <- sumN_inv.
                  FMap_simpl_step.
                  change value with ((fun '(_, v) => v) (from, value)).
                  rewrite sumN_inv.
                  rewrite <- (sumN_split _ _ _ (from, n)) by lia.
                  rewrite fin_maps.map_to_list_delete; auto.
          * unfold FMap.update.
            edestruct maybe_cases as [[-> ?H] | [-> _]].
            -- apply N.eq_add_0 in H3 as []; subst.
               edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  rewrite <- N.add_0_r.
                  change 0 with ((fun '(_, v) => v) (to, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  rewrite fin_maps.delete_notin; auto.
              --- rewrite N.sub_0_r.
                  rewrite <- N.add_0_r.
                  change 0 with ((fun '(_, v) => v) (to, 0)).
                  rewrite sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  FMap_simpl_step.
            -- edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite N.add_0_r.
                  rewrite fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  rewrite fin_maps.delete_notin; auto.
              --- FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite (sumN_split _ (to, value) (to, n)) by lia.
                  rewrite <- sumN_inv, fin_maps.map_to_list_delete.
                  2: FMap_simpl_step.
                  FMap_simpl_step.
                  change value with ((fun '(_, v) => v) (from, value)).
                  rewrite sumN_inv.
                  rewrite <- (sumN_split _ _ _ (from, 0)) by lia.
                  auto.
          * rewrite N.add_0_l.
            unfold FMap.update.
            edestruct maybe_cases as [[-> ->] | [-> _]].
            -- rewrite N.sub_0_r. cbn.
               rewrite fin_maps.delete_notin.
               2: FMap_simpl_step.
               rewrite fin_maps.delete_notin; auto.
            -- edestruct maybe_cases as [[-> ?H] | [-> _]].
              --- rewrite N.sub_0_le in H3; apply N.le_antisymm in H3; auto; subst.
                  FMap_simpl_step.
                  2: FMap_simpl_step. cbn.
                  rewrite fin_maps.delete_notin; auto.
              --- FMap_simpl_step.
                  2: FMap_simpl_step.
                  rewrite <- sumN_inv.
                  FMap_simpl_step.
                  change value with ((fun '(_, v) => v) (from, value)).
                  rewrite sumN_inv.
                  rewrite <- (sumN_split _ _ _ (from, 0)) by lia.
                  auto.
      + erewrite <- try_approve_preserves_total_supply; eauto.
        unfold sum_balances.
        erewrite <- try_approve_preserves_balances; eauto.
      + rename m into param.
        unfold sum_balances.
        contract_simpl.
        cbn.
        rewrite Z.ltb_ge in *.
        destruct (FMap.find (target param) _) eqn:target_balance; cbn.
        * assert (N_add_sub_move : forall n m p, p <= n -> n - p = m -> n = m + p) by lia.
          specialize (balance_le_sum_balances param.(target) cstate) as n_le_supply.
          rewrite target_balance in n_le_supply.
          cbn in n_le_supply.
          edestruct maybe_cases as [[-> quantity_eq] | [-> _]]; cbn.
        -- cbn in *.
            rewrite <- N2Z.id in quantity_eq.
            apply Z2N.inj in quantity_eq; auto.
            rewrite Z.add_move_0_l in quantity_eq.
            rewrite quantity_eq, Zabs2N.abs_N_nonneg, Z.add_opp_r, Z2N.inj_sub.
            apply N.add_sub_eq_l.
            rewrite !N2Z.id, N.add_comm.
            change n with ((fun '(_, v) => v) (target param, n)).
            now rewrite sumN_inv, fin_maps.map_to_list_delete by assumption.
            all: lia.
        -- rewrite FMap.elements_add_existing by eauto.
            cbn.
            rewrite N.add_comm.
            apply N_add_sub_move; try lia.
            rewrite <- Zabs2N.abs_N_nonneg by assumption.
            rewrite <- Zabs2N.inj_sub by (split; [assumption | lia]).
            rewrite Z.add_add_simpl_r_r, Zabs2N.inj_sub, !Zabs2N.id by lia.
            apply N.add_sub_eq_r.
            change n with ((fun '(_, v) => v) (target param, n)).
            now rewrite sumN_inv, fin_maps.map_to_list_delete by assumption.
        * edestruct maybe_cases as [[-> quantity_eq] | [-> _]]; cbn;
          unfold sum_balances in IH.
        -- rewrite fin_maps.delete_notin by auto.
            cbn in *.
            lia.
        -- rewrite FMap.elements_add by auto. cbn in *.
            lia.
      + try_solve_preserves_state.
      + try_solve_preserves_state.
      + try_solve_preserves_state.
      + now rewrite default_entrypoint_none in receive_some.
  Qed.