module SimpleFungibleToken;
  open import Anoma.Base;
  open import Stdlib.Prelude;

  import Stdlib.Data.String.Ord;

  open import Data.Int;

  import Data.Int.Ops;

  pair-from-optionString : (String  Int × Bool)  Maybe
    String  Int × Bool;
  pair-from-optionString := maybe (Int_0 , false);

  change-from-key : String  Int;
  change-from-key key := unwrap-default (read-post key)
    Data.Int.Ops.- unwrap-default (read-pre key);

  check-vp : List String  String  Int  String  Int × Bool;
  check-vp verifiers key change owner := if
    (change-from-key key Data.Int.Ops.< Int_0)
    (change Data.Int.Ops.+ change-from-key key
    , elem (Stdlib.Data.String.Ord.==) owner verifiers)
    (change Data.Int.Ops.+ change-from-key key , true);

  check-keys : String  List String  Int
    × Bool  String  Int × Bool;
  check-keys token verifiers (change , is-success) key := if
    is-success
    (pair-from-optionString
      (check-vp verifiers key change)
      (is-balance-key token key))
    (Int_0 , false);

  check-result : Int × Bool  Bool;
  check-result (change , all-checked) := change
      Data.Int.Ops.== Int_0
    && all-checked;

  vp : String  List String  List String  Bool;
  vp token keys-changed verifiers := check-result
    (foldl
      (check-keys token verifiers)
      (Int_0 , true)
      keys-changed);
end;