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;