(* 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_edukera.
Require Import fa12_edukera_spec.

Module FA12EdukeraVerif (C : ContractContext).

  Module fa12EdukeraSpec := FA12EdukeraSpec C.
  Import fa12EdukeraSpec.

  Import fa12AxiomsImpl fa12TypesImpl fa12DataImpl fa12Notations.
  Import self semantics.

  Opaque compare.
  Opaque map.update.

  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_edukera.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      ->
    fa12EdukeraSpec.spec env p sto ret_ops ret_sto.
  Proof.
    intros H_fuel.
    destruct sto as [allowances ledger].
    rewrite return_precond, eval_precond_correct.
    do 10 more_fuel; cbn.
    destruct p as [p | [p | [p | [p | p]]]]; cbn.
    - (* %getAllowance *)
      destruct p as [[sender spender] contract]; cbn.
      intros [allowance [H_allowance H]].
      rewrite H_allowance.
      injection H; intros H_ret_sto H_ret_ops.
      subst; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      intros [balance [H_balance H]].
      rewrite H_balance.
      injection H; intros H_ret_sto H_ret_ops.
      subst; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      intro H; injection H; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      intros [_ [_ [_ H]]].
      destruct (compare_equal _ _).
      all: cbn in H.
      2: destruct H as [_ [_ [_ H]]].
      2: destruct H as [allowance [H_allowance [H_amount_allowance H]]].
      2: change (@sender _ _) with (@sender self_type env) in H_allowance.
      2: rewrite H_allowance; clear H_allowance.
      all: destruct H as [from_balance [H_from_balance [H_amount_from_balance H]]].
      all: rewrite H_from_balance; clear H_from_balance.
      all: rewrite comparison_to_int_geq_Z in H_amount_from_balance.
      2: rewrite comparison_to_int_geq_Z in H_amount_allowance.
      all: split; auto.
      all: split with (Z.abs_N (Z.of_N from_balance - Z.of_N amount)).
      all: split; try lia.
      2: split; auto.
      2: split with (Z.abs_N (Z.of_N allowance - Z.of_N amount)).
      2: split; try lia.
      all: destruct map.mem eqn:H_to_balance.
      all: match goal with
        | [ _ : _ = true |- _ ] =>
          clear H_to_balance
        | [ _ : _ = false |- _ ] =>
          rewrite map.get_mem_false in H_to_balance
      end.
      all: match goal with
        | [ _ : exists _, _ |- _ ] =>
          destruct H as [to_balance [H_to_balance H]]
        | [_ : _ /\ _ |- _ ] =>
          destruct H as [_ H]
      end.
      all: rewrite H_to_balance; clear H_to_balance.
      all: injection H; clear H; intros H_ret_sto H_ret_ops.
      all: try rewrite N.add_0_l; auto.
    - (* %approve *)
      destruct p as [owner allowance']; cbn.
      all: destruct map.mem eqn:H_allowance.
      all: match goal with
        | [ _ : _ = true |- _ ] =>
          clear H_allowance
        | [ _ : _ = false |- _ ] =>
          rewrite map.get_mem_false in H_allowance
      end.
      all: intro H.
      all: match goal with
        | [ _ : exists _, _ |- _ ] =>
          destruct H as [allowance [H_allowance H]]
        | _ => auto
      end.
      all: change (@sender _ _) with (@sender self_type env) in H_allowance.
      all: rewrite H_allowance; clear H_allowance.
      1: destruct H as [H_allowance H].
      all: injection H; clear H; intros H_ret_sto H_ret_ops.
      2: auto.
      destruct allowance as [ | p1]; destruct allowance' as [ | p2].
      all: auto; discriminate.
  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) :
    fa12EdukeraSpec.spec env p sto ret_ops1 ret_sto1 ->
    fa12EdukeraSpec.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]]]]; cbn.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      intros [_ [H_ret_sto1 H_ret_ops1]] [_ [H_ret_sto H_ret_ops]].
      subst; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      intros [_ [H_ret_sto1 H_ret_ops1]] [_ [H_ret_sto H_ret_ops]].
      subst; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      intros [H_ret_sto1 H_ret_ops1] [H_ret_sto2 H_ret_ops2].
      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.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      intros [_ [H_ret_ops1 H_ret_sto1]] [_ [H_ret_ops2 H_ret_sto2]].
      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 ->
    fa12EdukeraSpec.spec env p sto ret_ops ret_sto
      ->
    precond (eval env fa12_edukera.main fuel ((p, sto), tt)) (fun _ => Logic.True).
  Proof.
    intros H_fuel.
    destruct sto as [ledger supply].
    rewrite eval_precond_correct.
    do 10 more_fuel; cbn.
    destruct p as [p | [p | [p | [p | p]]]]; cbn.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      destruct map.get as [allowance | ].
      all: intros [H_allowance H].
      all: destruct H_allowance.
      split with allowance; auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      destruct map.get as [balance | ].
      all: intros [H_balance H].
      all: destruct H_balance.
      split with balance; auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn; auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; cbn.
      destruct map.get as [from_balance | ]; cbn.
      all: intros [H_balance H].
      all: destruct H_balance.
      destruct H as [from_balance' [H_from_balance' H]].
      split with from_balance.
      split; auto.
      rewrite negb_false_iff, comparison_to_int_geq_N.
      split; try lia.
      destruct (compare_equal _ _)%Z; cbn.
      2: destruct map.get as [allowance | ].
      all: match goal with
        | [ _ : _ /\ (exists _, _) |- _ ] =>
          destruct H as [H_allowance H]
        | _ => auto
      end.
      all: match goal with
        | [ _ : exists _, _ |- _ ] =>
          destruct H_allowance
        | _ => auto
      end.
      2: destruct H as [allowance' [H_allowance' H]].
      all: clear H.
      2: split with allowance.
      2: split; auto.
      2: rewrite comparison_lt_ge_Z, comparison_to_int_geq_N.
      2: split; try lia.
      2: split with allowance.
      2: split; auto.
      2: rewrite comparison_to_int_geq_Z.
      2: split; try lia.
      all: split with from_balance.
      all: split; auto.
      all: rewrite comparison_to_int_geq_Z.
      all: split; try lia.
      all: destruct map.mem eqn:H_to_balance.
      all: auto.
      all: apply map.get_mem_true in H_to_balance.
      all: destruct H_to_balance as [to_balance H_to_balance].
      all: split with to_balance; auto.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      destruct map.mem eqn:H_allowance.
      2: auto.
      rewrite map.get_mem_true in H_allowance.
      destruct H_allowance as [allowance H_allowance].
      change (@sender _ _) with (@sender self_type env) in H_allowance.
      rewrite H_allowance.
      intros [H _].
      split with allowance.
      destruct allowance as [ | p1]; destruct allowance' as [ | p2].
      all: auto.
      destruct H as [H | H]; discriminate.
  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_edukera.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      <->
    fa12EdukeraSpec.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)) :
    fa12EdukeraSpec.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]]]]; cbn.
    all: destruct I.
    - (* %getAllowance *)
      destruct p as [[sender spender] contr]; cbn.
      intros [_ [H_ret_sto H_ret_ops]].
      auto.
    - (* %getBalance *)
      destruct p as [owner contr]; cbn.
      intros [_ [H_ret_sto H_ret_ops]].
      auto.
    - (* %getTotalSupply *)
      destruct p as [[] contr]; cbn.
      intros [H_ret_sto H_ret_ops].
      auto.
    - (* %transfer *)
      destruct p as [from [to amount]]; simpl.
      destruct (compare_equal (sender env) from) eqn:H_sender_from.
      1: rewrite eqb_eq in H_sender_from.
      all: intros [_ [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.
    - (* %approve *)
      destruct p as [spender allowance']; cbn.
      intros [H_allowance [H _]].
      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_edukera.main fuel ((p, sto), tt) = Return ((ret_ops, ret_sto), tt)
      ->
    storageValid ret_sto.
  Proof.
    intros H_fuel H_sto H_eval.
    assert (I : isSome (extract_fa12_ep p)).
    { destruct p as [p | [p | [p | [p | p]]]]; cbn.
      all: auto. }
    apply spec_if_impl in H_eval; auto.
    apply spec_fa12_correct with (I := I) in H_eval.
    apply sumOfAllBalances_constant in H_eval.
    unfold storageValid; rewrite H_eval; auto.
  Qed.

End FA12EdukeraVerif.