module Anoma.Internal.Transaction;

import Stdlib.Prelude open;

module DeltaComponent;
  
  type DeltaComponent :=
    mk {
      denom : Nat;
      sign : Bool;
      amount : Nat
    };
  
  zero : DeltaComponent :=
    mk@{
      denom := 0;
      sign := true;
      amount := 0
    };

  open DeltaComponent public;
end;

open DeltaComponent using {DeltaComponent} public;

Delta : Type := List DeltaComponent;

-- Proof, Resource, and Transaction are mutually recursive so they must be
-- defined in the same module.
module Helper;
  syntax alias Proof := Resource;
  syntax alias Commitment := Nat;
  syntax alias Nullifier := Nat;

  positive
  type Resource :=
    mkResource {
      logic : Resource -> Transaction -> Bool;
      label : Nat;
      quantity : Nat;
      data : Nat;
      eph : Bool;
      nonce : Nat;
      npk : Nat;
      rseed : Nat
    };

  type Transaction :=
    mkTransaction {
      roots : List Nat;
      commitments : List Commitment;
      nullifiers : List Nullifier;
      proofs : List Proof;
      delta : Delta;
      extra : Nat;
      -- TODO: Encoding of the preference function is not specified
      preference : Nat
    };
end;

module Transaction;
  syntax alias mk := Helper.mkTransaction;

  open Helper.Transaction public;
  open Helper using {Transaction} public;
end;

open Transaction using {Transaction} public;

module Resource;
  syntax alias mk := Helper.mkResource;

  open Helper.Resource public;
  open Helper using {Resource} public;
end;

open Resource using {Resource} public;