Defining the Application Specification

Tutorial Part 3: Defining the Application Specification

In the previous section, we defined our states and the validators that will manage them. Now, it's time to bring everything together into a single, top-level AppSpec. This specification is the source of truth for the entire application; it lists all the validators, defines the relationships between them, and enumerates all the valid user actions.

All the code for this section is in examples/Modsefa/Examples/Subscription/Spec.hs.

Step 1: Define the Application Type

First, we create a simple data type to serve as a unique identifier for our application.

Copydata SubscriptionApp

Step 2: Implement the AppSpec Typeclass

Next, we create an instance of the AppSpec typeclass for SubscriptionApp. This is where we define the complete architecture of our service.

Copyinstance AppSpec SubscriptionApp where 
  type Validators SubscriptionApp = 
    '[ 'Validator ServiceAndPricingValidator 
     , 'Validator CouponValidator 
     , 'Validator CustomerValidator 
     , 'Validator TreasuryValidator 
     ] 
  type AppStates SubscriptionApp = '["Uninitialized", "ServiceActive"] 
  type InitialAppState SubscriptionApp = "Uninitialized"
  type ActionTransitions SubscriptionApp = 
    '[ '(InitializeServiceSpec, "Uninitialized", "ServiceActive") 
     , '(CreatePricingTierSpec, "ServiceActive", "ServiceActive") 
     -- ... other actions 
     ]
  type AppInstanceParameters SubscriptionApp = 
    '[ '("ServiceAndPricingValidator", "bootstrapUtxo") ]
  type ParameterDerivations SubscriptionApp = 
    '[ 'DeriveParam "serviceValidatorAddress" 
          ('ValidatorAddress "ServiceAndPricingValidator") 
     , 'DeriveParam "derivedServiceProviderValidatorHash" 
          ('ValidatorHash "ServiceAndPricingValidator") 
     ]

Let's break down each of these associated types:

• Validators: This is a type-level list of all the validator specifications that are part of this application. We include all four of the validators we defined in the previous step.
• AppStates & InitialAppState: These define a simple, high-level state machine for the application itself. It can be either "Uninitialized" or "ServiceActive". This is useful for client-side logic and can also be used by the validator generator to determine how to apply constraints.
• ActionTransitions: This is a list of all the actions a user can perform. Each entry is a tuple containing the action's specification, the state the app must be in before the action, and the state the app will be in after the action. We will define the action specifications themselves in the next section.
• AppInstanceParameters: This defines the parameters that create a unique instance of the entire application. For our service, a unique instance is defined by the single bootstrapUtxo used to parameterize the main ServiceAndPricingValidator. All other parts of the application will be tied to this single instance.
• ParameterDerivations: This is one of the most powerful features for multi-validator apps. It tells Modsefa how to automatically derive parameters for one validator based on another. In our case:
  • It derives the serviceValidatorAddress by calculating the on-chain address of the ServiceAndPricingValidator. This derived value is then used to parameterize the CouponValidator and TreasuryValidator.
  • It also derives the hash of the ServiceAndPricingValidator, which is needed in the datum of the CustomerSubscriptionState.

This automatic derivation is what makes multi-validator coordination so seamless. We don't have to manually calculate and pass addresses between our contracts; the framework handles it for us, eliminating a major source of potential errors.

We have now fully specified the high-level architecture of our subscription application. We've defined our validators, established the relationships between them, and listed the actions that will be available to users.

In the next part, we will dive deep into the heart of the application: Part 4: Implementing the User Actions.