`phasOnlyOneTokenOfCurrencySymbol` using state machine

dummy.hs

data PState (s :: S)
  = PInitial
  | PFound
  | PFailed
  deriving stock
    ( Generic
    , Enum
    , Bounded
    )
  deriving anyclass
    ( PlutusType
    )

instance DerivePlutusType PState where
  type DPTStrat _ = PlutusTypeEnumData

f ::
  forall (kg :: KeyGuarantees) (ag :: AmountGuarantees) (s :: S).
  Term s (PCurrencySymbol :--> PValue kg ag :--> PBool)
f = plam $ \cs ((pto . pto) -> l :: Term _ (PBuiltinList _)) ->
  let isZeroAdaEntry ::
        Term
          _
          ( PBuiltinPair (PAsData PCurrencySymbol) (PAsData (PMap kg PTokenName PInteger))
              :--> PBool
          )
      isZeroAdaEntry = plam $ \pair ->
        let cs' = pfromData $ pfstBuiltin # pair
            isAda = ptraceIfFalse "Not ada" $ cs' #== padaSymbol

            tnMap = pfromData $ psndBuiltin # pair
            count = pfromData $ psndBuiltin # (ptryFromSingleton # pto tnMap)
            zeroAda = ptraceIfFalse "Non zero ada" $ count #== 0
         in isAda #&& zeroAda

      isNonAdaEntryValid ::
        Term
          _
          ( PBuiltinPair (PAsData PCurrencySymbol) (PAsData (PMap kg PTokenName PInteger))
              :--> PBool
          )
      isNonAdaEntryValid = plam $ \pair ->
        let cs' = pfromData $ pfstBuiltin # pair
            validCs = ptraceIfFalse "Unknown symbol" $ cs' #== cs

            tnMap = pfromData $ psndBuiltin # pair
            validTnMap = ptraceIfFalse "More than one token names or tokens" $
              pmatch (pfromSingleton # pto tnMap) $ \case
                PNothing -> pcon PFalse
                PJust ((pfromData . (psndBuiltin #)) -> tokenCount) ->
                  tokenCount #== 1
         in validCs #&& validTnMap

      go ::
        Term
          _
          ( (PState :--> PBuiltinList _ :--> PState)
              :--> PState
              :--> PBuiltinList _
              :--> PState
          )
      go = plam $ \self lastState ->
        pelimList
          ( \x xs -> pif
              (isZeroAdaEntry # x)
              (self # lastState # xs)
              $ pmatch lastState
              $ \case
                PInitial ->
                  pif
                    (isNonAdaEntryValid # x)
                    (self # pcon PFound # xs)
                    (pcon PFailed)
                PFound -> pcon PFailed
                PFailed -> ptraceError "unreachable"
          )
          ( pmatch lastState $ \case
              PFound -> lastState
              _ -> pcon PFailed
          )
   in pmatch (pfix # go # pcon PInitial # l) $
        \case
          PFound -> pcon PTrue
          _ -> pcon PFalse