Library ConCert.Examples.FA2.FA2Interface

From Stdlib Require Import ZArith.
From Stdlib Require Import String.
From Stdlib Require Import List. Import ListNotations.
From ConCert.Utils Require Import RecordUpdate.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Serializable.

Import DeriveSer.

Section FA2Interface.
  Context {BaseTypes : ChainBase}.
  Set Primitive Projections.
  Set Nonrecursive Elimination Schemes.

  Section FA2Types.

    Definition token_id := N.

    (* Dummy implementation of callbacks. *)
    Record callback (A : Type) := {
      blob : option A;
      return_addr : Address;
    }.

    Definition callback_addr {A : Type}
                             (c : callback A)
                             : Address :=
      c.(return_addr A).
    Global Coercion callback_addr : callback >-> Address.

    Record transfer_destination :=
      build_transfer_destination {
        to_ : Address;
        dst_token_id : N;
        amount : N;
    }.

    Record transfer :=
      build_transfer {
        from_ : Address;
        txs : list transfer_destination;
    }.

    Record balance_of_request := {
      owner : Address;
      bal_req_token_id : token_id;
    }.

    Record balance_of_response := {
      request : balance_of_request;
      balance : N;
    }.

    Record balance_of_param := {
      bal_requests : list balance_of_request;
      bal_callback : callback (list balance_of_response);
    }.

    Record token_metadata := {
      metadata_token_id : token_id;
      metadata_token_info : FMap string N
    }.

    Record operator_param := {
      op_param_owner : Address;
      op_param_operator : Address;
      op_param_token_id : token_id;
    }.

    Inductive update_operator :=
      | add_operator : operator_param -> update_operator
      | remove_operator : operator_param -> update_operator.

    Record transfer_destination_descriptor := {
      transfer_dst_descr_to_ : option Address;
      transfer_dst_descr_token_id : token_id;
      transfer_dst_descr_amount : N
    }.

    Record transfer_descriptor := {
      transfer_descr_from_ : option Address;
      transfer_descr_txs : list transfer_destination_descriptor
    }.

    Record transfer_descriptor_param := {
      transfer_descr_fa2 : Address;
      transfer_descr_batch : list transfer_descriptor;
      transfer_descr_operator : Address;
    }.

    Inductive fa2_token_receiver :=
      | tokens_received : transfer_descriptor_param -> fa2_token_receiver.

    Inductive fa2_token_sender :=
      | tokens_sent : transfer_descriptor_param -> fa2_token_sender.

  End FA2Types.

  Section Setters.

    MetaRocq Run (make_setters transfer_destination).
    MetaRocq Run (make_setters transfer).
    MetaRocq Run (make_setters balance_of_request).
    MetaRocq Run (make_setters balance_of_response).
    MetaRocq Run (make_setters balance_of_param).
    MetaRocq Run (make_setters token_metadata).
    MetaRocq Run (make_setters operator_param).
    MetaRocq Run (make_setters transfer_destination_descriptor).
    MetaRocq Run (make_setters transfer_descriptor).
    MetaRocq Run (make_setters transfer_descriptor_param).

  End Setters.

  Section Serialization.

    Instance callback_serializable {A : Type} `{serA : Serializable A} : Serializable (callback A) := Derive Ser.

    Global Instance transfer_destination_serializable : Serializable transfer_destination := Derive Ser.

    Global Instance transfer_serializable : Serializable transfer := Derive Ser.

    Global Instance balance_of_request_serializable : Serializable balance_of_request := Derive Ser.

    Global Instance balance_of_response_serializable : Serializable balance_of_response := Derive Ser.

    Instance bal_of_param_callback_serializable : Serializable (callback (list balance_of_response)) := Derive Ser.

    Global Instance balance_of_param_serializable : Serializable balance_of_param := Derive Ser.

    Global Instance token_metadata_serializable : Serializable token_metadata := Derive Ser.

    Instance metadata_callback_serializable : Serializable (callback (list token_metadata)) := Derive Ser.

    Global Instance operator_param_serializable : Serializable operator_param := Derive Ser.

    Global Instance update_operator_serializable : Serializable update_operator := Derive Ser.

    Global Instance transfer_destination_descriptor_serializable : Serializable transfer_destination_descriptor := Derive Ser.

    Global Instance transfer_descriptor_serializable : Serializable transfer_descriptor := Derive Ser.

    Global Instance transfer_descriptor_param_serializable : Serializable transfer_descriptor_param := Derive Ser.

    Global Instance fa2_token_receiver_serializable : Serializable fa2_token_receiver := Derive Ser.

    Global Instance fa2_token_sender_serializable : Serializable fa2_token_sender := Derive Ser.

    Instance transfer_descriptor_param_callback_serializable : Serializable (callback transfer_descriptor_param) := Derive Ser.
  End Serialization.
End FA2Interface.