1. CEK Machine Tutorial : Mockup Demo - wimsio/universities GitHub Wiki

Table of Contents

  1. Introduction

  2. Installing and Running

  3. Understanding the Code Structure

    1. 3.1 Term Language
    2. 3.2 Costing Modes
    3. 3.3 Emitter Modes
    4. 3.4 Errors and Results
    5. 3.5 Machine State

  4. Evaluating Terms

    1. 4.1 Constants and Variables
    2. 4.2 Lambdas and Application
    3. 4.3 Builtin Functions

  5. Experimenting with Costing and Logging

    1. 5.1 Changing Costing Modes
    2. 5.2 Changing Emitter Modes

  6. Handling Errors

  7. Exercises

  8. Glossary

1. Introduction

This tutorial walks you through a minimal, educational CEK (Control-Environment-Kontinuation) machine written in Haskell, inspired by Cardano’s Plutus smart contract engine. You’ll learn how terms are built and evaluated, how resource costing and logging work, and how to test and extend the machine.

2. Installing and Running

  1. Copy the CEK mockup code from above into a file named Main.hs.

  2. Make sure you have GHC installed.

  3. Run the code with:

    runghc Main.hs

    or

    ghc Main.hs && ./Main

You’ll see evaluation results, budgets, and logs for built-in test cases.

3. Understanding the Code Structure

3.1 Term Language

The machine works on a simple term language with:

  • Variables (Var)
  • Lambdas (Lam)
  • Application (App)
  • Constants (Const)
  • Builtins (Builtin, BuiltinAdd, BuiltinMul)

Example: (\x -> x + 1) 41 is represented as:

App (Lam "x" (App (App (Builtin "addInteger") (Var "x")) (Const 1))) (Const 41)

3.2 Costing Modes

  • Counting: Totals up all resource usage (no upper limit).
  • Restricting: Sets a maximum CPU and memory limit—evaluation fails if the script exceeds it.

3.3 Emitter Modes

  • NoEmitter: No logs at all.
  • LogEmitter: Step-by-step logs.
  • LogWithBudgetEmitter: Logs with current budget at every step.

3.4 Errors and Results

  • Structural errors: Like unbound variables.
  • Operational errors: Like applying a non-function.
  • OutOfBudget: When evaluation exceeds the allowed cost.

3.5 Machine State

Keeps track of:

  • The current variable environment.
  • The accumulated cost.
  • The logs.
  • The chosen costing and emitter modes.

4. Evaluating Terms

4.1 Constants and Variables

Evaluate constants or lookup variables:

Const 42         -- Integer constant 42
Var "x"          -- Variable named "x"

If a variable is unbound, you’ll see a structural error.

4.2 Lambdas and Application

Lambdas:

Lam "x" (Var "x")   -- The identity function: \x -> x

Applications: Apply a function to an argument:

App (Lam "x" (Var "x")) (Const 5)  -- Evaluates to Const 5

Nested functions:

App (App (Lam "x" (Lam "y" (App (App (Builtin "addInteger") (Var "x")) (Var "y")))) (Const 10)) (Const 20)

This is equivalent to (\x -> (\y -> x + y)) 10 20.

4.3 Builtin Functions

Supports simple arithmetic builtins:

  • "addInteger": addition
  • "multiplyInteger": multiplication

To add two numbers:

App (App (Builtin "addInteger") (Const 1)) (Const 2)  -- Evaluates to Const 3

5. Experimenting with Costing and Logging

5.1 Changing Costing Modes

  • Unlimited resources:

    runCEK Counting LogWithBudgetEmitter term

  • Limited budget (e.g., 5 CPU, 5 MEM):

    runCEK (Restricting (ExBudget 5 5)) LogWithBudgetEmitter term

If the script exceeds the budget, you’ll see an OutOfBudget error.

5.2 Changing Emitter Modes

Try swapping emitter modes to see how logging changes:

  • No logs: NoEmitter
  • Step logs: LogEmitter
  • Logs with resource usage: LogWithBudgetEmitter

6. Handling Errors

  • Unbound variable:

    Var "z"

    This will produce a StructuralError.

  • Applying non-function:

    App (Const 2) (Const 3)

    This will produce an OperationalError.

  • Budget exceeded: If costing mode is Restricting and term is complex or the budget is too small.

7. Exercises

  1. Exercise 1: Write a term for (\x -> x * 2) 6 and run it with unlimited budget and with a tight budget.
  2. Exercise 2: Change the emitter mode to show step-by-step logs for test2.
  3. Exercise 3: Try applying a built-in to the wrong type of term (e.g., addInteger to a lambda), and observe the error.

8. Glossary

Term Meaning
CEK Machine Abstract machine for evaluating terms, tracking environment and budget.
Term The language the CEK machine understands (constants, lambdas, etc.)
CostingMode How cost/budget is tracked (Counting, Restricting)
EmitterMode Logging style: none, step, or step+budget
MachineState All current info needed for evaluation
StructuralError Something is wrong with how the program is written
OperationalError The logic is invalid at runtime (e.g., wrong application)
OutOfBudget Script used too much resource
Env Variable bindings (names to values)
Partial Application Applying a built-in to only some of its arguments
App Function application in the term language
Lam Lambda abstraction (function definition)