Defining the Application Specification

Tutorial Part 3: Defining the Application Specification

In the previous section, we defined our states and the single validator that will manage them. Now, we'll bring them together in the top-level AppSpec. This specification is the complete blueprint for our Feed App, defining its architecture, its state machine, and all the valid user actions.

All the code for this section is in examples/Modsefa/Examples/Feed/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 FeedApp

Step 2: Implement the AppSpec Typeclass

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

Copyinstance AppSpec FeedApp where
  type Validators FeedApp =
    '[ 'Validator FeedValidator
     ]
  type AppStates FeedApp = '["Uninitialized", "Initialized"]
  type InitialAppState FeedApp = "Uninitialized"
  type ActionTransitions FeedApp =
    '[ '(InitializeFeedSpec, "Uninitialized", "Initialized")
     , '(UpdateFeedSpec, "Initialized", "Initialized")
     ]
  type AppInstanceParameters FeedApp =
    '[ '("FeedValidator", "bootstrapUtxo")
     ]
  type ParameterDerivations FeedApp = '[]

Let's break down what each of these associated types means for our Feed App:

• Validators: This is a type-level list of all validators in the application. For our simple app, it contains only our single FeedValidator.
• AppStates & InitialAppState: These define a simple state machine for the application. Our feed can be "Uninitialized" before the first action, and "Initialized" after. This helps define which actions are valid at which times.
• ActionTransitions: This lists all the actions a user can perform. For the Feed App, there are two:
  1. InitializeFeedSpec: This action can only be performed when the app is "Uninitialized", and it transitions the app to the "Initialized" state.
  2. UpdateFeedSpec: This action can only be performed when the app is already "Initialized", and it leaves the app in the "Initialized" state.
• AppInstanceParameters: This defines how a unique instance of our application is created on the blockchain. For the Feed App, a unique instance is identified by the bootstrapUtxo that is used to parameterize our FeedValidator.
• ParameterDerivations: This is used for coordinating multiple validators. Since our Feed App only has one validator, this list is empty ('[]).

We have now fully specified the architecture of our Feed App. We've defined our validator and established the actions that users will be able to perform.

In the next part, we will look at the specifications for the InitializeFeedSpec and UpdateFeedSpec actions themselves.