(* Open Source License *)
(* Copyright (c) 2021 Nomadic Labs. <contact@nomadic-labs.com> *)

(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)

(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)

(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)

Require Import NArith.
Require Import ZArith.
Require Import Bool.
Require Import String.
Require Import List.
Require Import syntax.
Require Import semantics.
Require Import comparable.
Require Import error.
Require Import Lia.
Require Import util.
Require Import utils.
Require Import fa12_interface.
Require Import fa12_spec.
Require Import fa12_verification.
Require Import fa12_dexter.
Require Import fa12_dexter_spec.

Module FA12DexterVerif (C : ContractContext).

  Module fa12DexterSpec := FA12DexterSpec C.
  Import fa12DexterSpec.

  Import fa12AxiomsImpl fa12TypesImpl fa12DataImpl fa12Notations.
  Import self semantics.

  Opaque compare.

  Lemma spec_if_impl
        (env : @proto_env self_type)
        (fuel : Datatypes.nat)
        (p : data parameter_ty)
        (sto : data storage_ty)
        (ret_ops : data (list operation))
        (ret_sto : data storage_ty) :
    50 <= fuel ->
    eval env fa12_dexter.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      ->
    fa12DexterSpec.spec env p sto ret_ops ret_sto.
  Proof.
    intros H_fuel.
    destruct sto as [ledger [allowances [admin supply]]].
    rewrite return_precond, eval_precond_correct.
    do 10 more_fuel; cbn.
    destruct p as [[[p | p] | [p | p]] | [p | p]]; cbn.
    all: intros [H_amount H].
    all: rewrite negb_false_iff, eqb_eq in H_amount.
    all: split; auto.
    all: clear H_amount.
    - (* %approve *)
      destruct p as [owner allowance']; cbn.
      destruct map.get as [allowance | ]; cbn.
      all: destruct (compare_equal _ _) eqn:H_allowance'_0.
      all: destruct H as [H_allowance H].
      all: injection H; intros H_ret_sto H_ret_ops.
      1: rewrite eqb_eq in H_allowance'_0; subst.
      all: auto.
      destruct allowance as [ | p1]; destruct allowance' as [ | p2].
      all: auto; discriminate.
    - (* %getAllowance *)
      destruct p as [[sender spender] contract]; cbn.
      destruct map.get as [allowance | ]; cbn.
      all: injection H; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      destruct map.get as [balance | ]; cbn.
      all: injection H; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      injection H; auto.
    - (* %mintOrBurn *)
      destruct p as [amount owner]; cbn.
      destruct H as [H_admin H].
      rewrite negb_false_iff, eqb_eq in H_admin.
      split; auto.
      clear H_admin.
      destruct map.get as [balance | ]; cbn.
      all: destruct (_ >=? 0)%Z eqn:H_amount_balance.
      all: destruct H as [balance' [H_balance' H]].
      all: try discriminate.
      all: apply map.unsome in H_balance'.
      all: rewrite Z.geb_le in H_amount_balance.
      all: simpl in H.
      all: split with balance'.
      all: split; try lia.
      all: destruct (compare_equal _ _).
      all: injection H; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      destruct (compare_equal _ _) eqn:H_sender_from.
      2: destruct map.get as [allowance | ].
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct (_ >=? _)%Z eqn:H_amount_allowance
        | _ => auto
      end.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct H as [allowance' [H_allowance' H]]
        | _ => auto
      end.
      all: try discriminate.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          rewrite Z.geb_le in H_amount_allowance
        | _ => auto
      end.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          apply map.unsome in H_allowance'
        | _ => auto
      end.
      all: unfold stack_dig in H; cbn in H.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct (compare_equal _ _) eqn:H_allowance'_0 in H
        | _ => auto
      end.
      all: destruct map.get as [from_balance | ].
      all: destruct (_ >=? _)%Z eqn:H_amount_from_balance.
      all: destruct H as [from_balance' [H_from_balance' H]].
      all: try discriminate.
      all: rewrite Z.geb_le in H_amount_from_balance.
      all: apply map.unsome in H_from_balance'.
      all: destruct (compare_equal _ _) eqn:H_from_balance'_0 in H.
      all: split with from_balance'; split.
      all: try lia.
      all: match goal with
        | [ _ : _ |- exists _, _ ] =>
          split with allowance'; split
        | _ => auto
      end.
      all: try lia.
      all: rewrite H_from_balance'_0.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          rewrite H_allowance'_0
        | _ => auto
      end.
      all: destruct map.get as [to_balance | ].
      all: try rewrite N.add_0_l.
      all: destruct (compare_equal _ _) eqn:H_to_balance'_0 in H.
      all: rewrite H_to_balance'_0.
      all: injection H; auto.
  Qed.

  Lemma spec_unique
        (env : @proto_env self_type)
        (p : data parameter_ty)
        (sto : data storage_ty)
        (ret_ops1 : data (list operation))
        (ret_ops2 : data (list operation))
        (ret_sto1 : data storage_ty)
        (ret_sto2 : data storage_ty) :
    fa12DexterSpec.spec env p sto ret_ops1 ret_sto1 ->
    fa12DexterSpec.spec env p sto ret_ops2 ret_sto2 ->
    ret_sto1 = ret_sto2 /\ ret_ops1 = ret_ops2.
  Proof.
    destruct p as [[[p | p] | [p | p]] | [p | p]]; cbn.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      intros [_ [_ [H_ret_sto1 H_ret_ops1]]].
      intros [_ [_ [H_ret_sto2 H_ret_ops2]]].
      subst; auto.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      intros [_ [H_ret_sto1 H_ret_ops1]].
      intros [_ [H_ret_sto2 H_ret_ops2]].
      subst; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      intros [_ [H_ret_sto1 H_ret_ops1]].
      intros [_ [H_ret_sto2 H_ret_ops2]].
      subst; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      intros [_ [H_ret_sto1 H_ret_ops1]].
      intros [_ [H_ret_sto2 H_ret_ops2]].
      subst; auto.
    - (* %mintOrBurn *)
      destruct p as [amount owner]; cbn.
      intros [_ [_ [balance1 [H_balance1 [H_ret_sto1 H_ret_ops1]]]]].
      intros [_ [_ [balance2 [H_balance2 [H_ret_sto2 H_ret_ops2]]]]].
      assert (H_balance : balance1 = balance2).
      { lia. }
      subst; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      intros [_ [balance1 [H_balance1 H1]]].
      intros [_ [balance2 [H_balance2 H2]]].
      assert (H_balance : balance1 = balance2).
      { lia. }
      destruct (compare_equal _ _).
      2: destruct H1 as [allowance1 [H_allowance1 H1]].
      2: destruct H2 as [allowance2 [H_allowance2 H2]].
      all: destruct H1 as [H_ret_sto1 H_ret_ops1].
      all: destruct H2 as [H_ret_sto2 H_ret_ops2].
      all: subst; auto.
      assert (H_allowance : allowance1 = allowance2).
      { lia. }
      subst; auto.
  Qed.

  Lemma spec_success
        (env : @proto_env self_type)
        (fuel : Datatypes.nat)
        (p : data parameter_ty)
        (sto : data storage_ty)
        (ret_ops : data (list operation))
        (ret_sto : data storage_ty) :
    50 <= fuel ->
    fa12DexterSpec.spec env p sto ret_ops ret_sto
      ->
    precond (eval env fa12_dexter.main fuel ((p, sto), tt)) (fun _ => Logic.True).
  Proof.
    intros H_fuel.
    destruct sto as [ledger [allowances [admin supply]]].
    rewrite eval_precond_correct.
    all: do 10 more_fuel; cbn.
    destruct p as [[[p | p] | [p | p]] | [p | p]]; cbn.
    all: intros [H_amount H].
    all: rewrite negb_false_iff, eqb_eq.
    all: split; auto.
    all: clear H_amount.
    all: revert H.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      intros [H _].
      destruct map.get as [allowance | ]; cbn.
      all: destruct (compare_equal _ _).
      all: destruct allowance' as [ | p1]; auto.
      all: destruct allowance as [ | p2]; auto.
      all: destruct H; discriminate.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      destruct map.get as [allowance | ]; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      destruct map.get as [balance | ]; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn; auto.
    - (* %mintOrBurn *)
      destruct p as [amount owner]; cbn.
      intros [H_admin [balance' [H_balance' _]]].
      rewrite negb_false_iff, eqb_eq.
      split; auto.
      clear H_admin.
      destruct map.get as [balance | ].
      all: destruct (_ >=? _)%Z eqn:H_balance_amount.
      all: try rewrite comparison_ge_lt_Z, Z.ltb_lt in H_balance_amount.
      all: try lia.
      all: split with balance'; split.
      all: try f_equal; try lia.
      all: simpl.
      all: destruct (compare_equal _ _); auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      destruct (compare_equal _ _) eqn:H_sender_from.
      all: destruct map.get as [from_balance | ] eqn:H_from_balance.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct map.get as [allowance | ] eqn:H_allowance at 1 2
        | _ => auto
      end.
      all: intros [from_balance' [H_from_balance' H]].
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct H as [allowance' [H_allowance' H]]
        | _ => auto
      end.
      all: clear H.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct (_ >=? _)%Z eqn:H_allowance_amount
        | _ => auto
      end.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          rewrite comparison_ge_lt_Z, Z.ltb_lt in H_allowance_amount
        | _ => auto
      end.
      all: try lia.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          split with allowance'; split
        | _ => auto
      end.
      all: try (f_equal; lia).
      all: unfold stack_dig; cbn.
      all: match goal with
        | [ _ : _ = false |- _ ] =>
          destruct (compare_equal _ _) eqn:H_allowance'_0 at 1
        | _ => auto
      end.
      all: try rewrite H_from_balance.
      all: destruct (_ >=? _)%Z eqn:H_from_balance_amount at 1.
      all: try rewrite comparison_ge_lt_Z, Z.ltb_lt in H_from_balance_amount.
      all: try lia.
      all: split with from_balance'; split.
      all: try (f_equal; lia).
      all: destruct (compare_equal _ _) eqn:H_balance'_0 at 1.
      all: destruct map.get as [to_balance | ] at 1.
      all: destruct (compare_equal _ _) at 1.
      all: auto.
  Qed.

  Module fa12SpecIffImpl := FA12SpecIffImpl C.
  Import fa12SpecIffImpl.

  Theorem impl_correct
          (env : @proto_env self_type)
          (fuel : Datatypes.nat)
          (p : data parameter_ty)
          (sto : data storage_ty)
          (ret_ops : data (list operation))
          (ret_sto : data storage_ty) :
    50 <= fuel ->
    eval env fa12_dexter.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      <->
    fa12DexterSpec.spec env p sto ret_ops ret_sto.
  Proof.
    intros H_fuel.
    eapply spec_iff_impl with (fuel_bound := 50); auto.
    - apply spec_if_impl.
    - apply spec_unique.
    - apply spec_success.
  Qed.

  Module FA12SumOfBalances := FA12SumOfBalances C fa12TypesImpl fa12DataImpl fa12AxiomsImpl.
  Import FA12SumOfBalances.

  Theorem spec_fa12_correct
          (env : @proto_env self_type)
          (p : data parameter_ty)
          (sto : data storage_ty)
          (ret_ops : data (list operation))
          (ret_sto : data storage_ty)
          (I : isSome (extract_fa12_ep p)) :
    fa12DexterSpec.spec env p sto ret_ops ret_sto ->
    fa12Spec.main env (get_opt (extract_fa12_ep p) I) sto ret_ops ret_sto.
  Proof.
    destruct p as [[[p | p] | [p | p]] | [p | p]]; cbn.
    all: destruct I; cbn.
    all: intros [H_amount H].
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      destruct H as [H_allowance [H _]].
      auto.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      destruct H as [H_ret_sto H_ret_ops].
      rewrite H_amount; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      destruct H as [H_ret_sto H_ret_ops].
      rewrite H_amount; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      destruct H as [H_ret_sto H_ret_ops].
      rewrite H_amount; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      destruct (compare_equal _ _) eqn:H_sender_from.
      1: rewrite eqb_eq in H_sender_from.
      all: destruct H as [from_balance' [H_from_balance' H]].
      2: destruct H as [allowance' [H_allowance H]].
      all: destruct H as [H_ret_sto _].
      all: split with from_balance'.
      all: split; auto.
      apply or_intror.
      split with allowance'; auto.
  Qed.

  Theorem storage_valid
          (env : @proto_env self_type)
          (fuel : Datatypes.nat)
          (p : data parameter_ty)
          (sto : data storage_ty)
          (ret_ops : data (list operation))
          (ret_sto : data storage_ty) :
    50 <= fuel ->
    storageValid sto ->
    eval env fa12_dexter.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      ->
    storageValid ret_sto.
  Proof.
    intros H_fuel H_sto H_eval.
    apply spec_if_impl in H_eval; auto.
    assert (I : isSome (extract_fa12_ep p) \/ storageValid ret_sto).
    all: destruct sto as [ledger [allowances [admin supply]]].
    2: destruct I as [I | I]; auto.
    2: pose proof H_eval as H_spec.
    2: apply spec_fa12_correct with (I := I) in H_spec.
    2: apply sumOfAllBalances_constant in H_spec.
    all: unfold storageValid.
    2: rewrite H_spec, <-H_sto.
    2: clear H_spec H_sto.
    all: destruct p as [[[p | p] | [p | p]] | [p | p]]; cbn.
    all: auto.
    all: revert H_eval.
    1:{ (* %mintOrBurn *)
        destruct p as [amount owner]; cbn.
        intros [_ [_ [balance' [H_balance' [H _]]]]].
        apply or_intror.
        subst.
        rewrite sumOfAllBalances_setBalance.
        rewrite <-H_sto.
        cbn in H_balance'; cbn.
        destruct map.get as [balance | ].
        all: lia. }
    all: destruct I.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      intros [_ [_ [H _]]].
      all: subst; auto.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      intros [_ [H _]].
      subst; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      intros [_ [H _]].
      subst; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      intros [_ [H _]].
      subst; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      intros [_ [from_balance' [_ H]]].
      destruct (compare_equal _ _).
      2: destruct H as [allowance' [_ H]].
      all: destruct H as [H _].
      all: subst; auto.
  Qed.

End FA12DexterVerif.