Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate ScalarAccount; do not edit.
module Generated.AggregateScalarExpressions.ScalarAccount.Transducer
  ( scalarAccountTransducer
  , scalarAccountFoldFingerprint
  , BehaviorOwnership (..)
  , scalarAccountPredicateVerifications
  ) where

import Generated.AggregateScalarExpressions.ScalarAccount.Domain
import Data.Text (Text)
import Data.Time.Calendar (fromGregorian)
import Data.Time.Clock (UTCTime (..), picosecondsToDiffTime)
import Generated.AggregateScalarExpressions.Nominals (AccountMode (..), RequestId, parseRequestId)
import Generated.AggregateScalarExpressions.StructuralProjections qualified as StructuralProjections
import Generated.AggregateScalarExpressions.Nominals qualified as GeneratedNominals
import ScalarExpressions.Domain qualified
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer, (.*), (.+), (.-), (.==), (.<=), (.>=), (.&&))
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S
import AggregateScalarExpressions.ScalarAccount.Holes qualified as Holes
import Data.Text qualified as T
import Keiki.Builder ((=:))
import Keiki.Generics (RegFieldsOf)
import Keiro.Snapshot.Codec (FoldVersion (..))

scalarAccountTransducer
  :: SymTransducer
       (HsPred ScalarAccountRegs ScalarAccountCommand)
       ScalarAccountRegs
       ScalarAccountVertex
       ScalarAccountCommand
       ScalarAccountEvent
scalarAccountTransducer =
  B.buildTransducer ScalarAccountOpen initialScalarAccountRegs isTerminal do
    B.from ScalarAccountOpen do
      B.onCmd inCtorAdjust $ \d -> B.do
        let commandLimitsMinimum = K.inpProj StructuralProjections.limitsMinimumWitness inCtorAdjust (#limits :: K.Index (RegFieldsOf AdjustData) ScalarExpressions.Domain.Limits)
            registerLimitsMinimum = K.regProj StructuralProjections.limitsMinimumWitness (#limits :: K.Index ScalarAccountRegs ScalarExpressions.Domain.Limits)
            commandMode = K.inpProj GeneratedNominals.accountModeEqualityWitness inCtorAdjust (#mode :: K.Index (RegFieldsOf AdjustData) AccountMode)
            registerMode = K.regProj GeneratedNominals.accountModeEqualityWitness (#mode :: K.Index ScalarAccountRegs AccountMode)
            commandRequestId = K.inpProj GeneratedNominals.requestIdEqualityWitness inCtorAdjust (#requestId :: K.Index (RegFieldsOf AdjustData) RequestId)
            registerRequestId = K.regProj GeneratedNominals.requestIdEqualityWitness (#requestId :: K.Index ScalarAccountRegs RequestId)
        B.requireGuard $
          (((((d.balance .+ B.reg @"balance" .>= K.lit (-100 :: Integer)
          .&& B.reg @"reserved" .+ d.requested .<= B.reg @"capacity")
          .&& d.observedAt .>= B.reg @"openedAt")
          .&& commandLimitsMinimum .>= registerLimitsMinimum)
          .&& d.active .== K.lit False)
          .&& commandMode .== registerMode)
          .&& commandRequestId .== registerRequestId
        B.slot @"balance" =: (B.reg @"balance" .+ d.balance .* K.lit (2 :: Integer))
        B.slot @"reserved" =: (B.reg @"reserved" .+ (d.requested .- B.reg @"capacity"))
        B.slot @"machine" =: K.lit (-7 :: Int)
        B.slot @"label" =: K.lit ("adjusted" :: Text)
        B.slot @"active" =: K.lit True
        B.slot @"mode" =: K.lit Restricted
        B.slot @"requestId" =: K.lit (case parseRequestId "req_01h455vb4pex5vsknk084sn02q" of Right parsed -> parsed; Left _ -> error "validated ID literal failed to parse")
        B.slot @"openedAt" =: K.lit (UTCTime (fromGregorian 2026 2 3) (picosecondsToDiffTime 14706000000000000))
        B.slot @"limits" =: d.limits
        B.emit wireAdjusted (AdjustedTermFields
          { balance = d.balance
          , requested = d.requested
          , machine = d.machine
          , label = d.label
          , active = d.active
          , mode = d.mode
          , requestId = d.requestId
          , observedAt = d.observedAt
          , limits = d.limits
          })
        B.goto ScalarAccountReviewed
    B.from ScalarAccountReviewed do
      B.onCmd inCtorClose $ \d -> B.do
        Holes.transition2ReviewedCloseHole d
        B.emit wireClosedEvent (ClosedEventTermFields
          { balance = d.balance
          })
        B.goto ScalarAccountClosed
 where
  isTerminal = \case
    ScalarAccountClosed -> True
    _ -> False

scalarAccountFoldFingerprint :: Text
scalarAccountFoldFingerprint = T.intercalate "|" ("60f4f059f718b2ee2bca06360ea20221" : [foldToken Holes.transition2ReviewedCloseHoleFoldVersion] ) where foldToken (FoldVersion token) = T.pack (show (T.length token)) <> ":" <> token

data BehaviorOwnership = GeneratedOwned | HoleOwned
  deriving stock (Eq, Show)

-- Every checked transition predicate is audited through Keiki's conservative
-- symbolic verifier. Opaque Hole terms remain explicitly unverified.
scalarAccountPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
scalarAccountPredicateVerifications = sequence
  [ verifyTransition "transition1OpenAdjust" GeneratedOwned ScalarAccountOpen 0
  , verifyTransition "transition2ReviewedClose" HoleOwned ScalarAccountReviewed 0
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut scalarAccountTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")