The Modsefa Spec: Types for Guarantees, Values for Code-Gen

In the last post, I explained the core idea behind Modsefa: viewing a dApp as a single specification rather than two separate (on-chain and off-chain) codebases.

This approach is powerful, but it leads to a key question: how does this actually work? How does a high-level definition turn into both a secure validator script and a type-safe client library?

The answer is a compilation pipeline that runs "under the hood". But the most important point is this: as an app developer, you don't need to know how this complex engine works. You just need to write your specification using the Modsefa DSL, which is specifically designed to be simple and to help you express your required logic clearly. The DSL is the interface that hides the complexity.

For those curious about the "how" it works, this post introduces that engine. The architecture takes your single spec and runs it down two parallel tracks, which are designed to handle two very different levels of complexity.

Stages 1 & 2: The Single Source of Truth

The pipeline starts with the high-level specification that you, the app developer, write using the Modsefa DSL. This is where you define your dApp's logic at the type level. The Haskell type-checker validates this spec for you, catching consistency errors before you ever generate code.

This type-level spec is then "reified" into a value-level singleton spec—a rich, complex Haskell value that represents your entire dApp. This value is the single root from which both generation tracks begin.

From here, the pipeline forks.

Generation Track A: The Off-Chain Client (The Direct Path)

This track is responsible for the client-side transaction builder. Its job is to take a high-level "Action" that you've defined (along with its parameters) and convert it into a concrete, low-level Cardano transaction.

This translation process involves converting your abstract intent, like "operations on state" or "constraints", into the specific inputs, outputs, datums, redeemers, and minting policies that a transaction requires.

This is a "Haskell-to-Haskell" operation. The transaction builder is a Haskell function that reads the full, rich, value-level singleton spec directly. It has all the information it needs in a format it already understands. Because this task is about translating one action at a time, it is far less complex than generating the entire validator.

Generation Track B: The On-Chain Validator (The Compiler Path)

This track is responsible for creating the secure, on-chain Plutus scripts for each validator in your application. This task is fundamentally more complex than the client-side translation.

A single validator script doesn't necessarily need to know about all actions in the entire application, but it must contain the logic to validate all the actions that are associated with it in the spec.

This means the generator's job is to perform a "many-to-one" compilation (for each validator in an application): it must take the set of actions defined for a validator and compile them into a single script. This script must be able to:

Identify which action is being attempted (by inspecting the redeemer).
Branch to the correct validation logic for that specific action.

This is where the Intermediate Representation (IR) becomes essential.

First, a compiler translates the complex Singleton Spec into the AppIR. This IR is a "snapshot" of the entire application's on-chain logic, and it's structured in a way that maps sets of actions to the specific validators that must handle them.

This IR serves two critical purposes:

A Target for Optimization: Generating efficient, minimal validator code is vital for on-chain execution. The IR is a data structure specifically designed to be analyzed and optimized. We can run passes over this IR to simplify the logic for each action's branch before we generate the final, expensive Plutus script.
Separation of Concerns: The IR acts as a clean, stable interface. It "flattens" the complex, type-driven spec into a more straightforward description of logic (e.g., "This validator handles these three actions"). This allows the final validator generator to be much simpler: its only job is to translate this stable IR into Plutus, not to understand the entire complex singleton machinery.

Conclusion

This "spec-first," two-track pipeline is what makes the Modsefa DSL possible.

You, the developer, get to live in the simple, expressive world of the DSL. Under the hood, the pipeline splits to handle the two different tasks:

The Client Generator takes the simple, direct path, reading the rich singleton spec to translate one "Action" into one "Transaction." The IR is not needed for this simpler task.
The Validator Generator takes the more complex path, using the IR as a crucial tool for optimization and for managing the complexity of compiling a set of actions into a single, efficient validator script.

This split is the core of the architecture. It's how one source of truth can power two very different artifacts by using the right tool for each job.