4. CEK Machine Tutorial : Plutus Evaluating Plutus Core Lambda Expressions & Applications with the CEK Machine

Table of Contents

1. Introduction

2. Costing and Emitter Modes Overview

   1. Costing Modes Recap
   2. Emitter Modes Recap

3. Running the Demo Script

4. Understanding Evaluation Results

5. Sample Output

6. Experimentation Guidelines

7. Costing & Logging Summary Table

8. Challenge Exercises

9. Plutus Core Lambda and Application Structure

   1. Lambda Expressions in Plutus Core
   2. Application in Plutus Core
   3. Evaluating: Identity Function Example
   4. Lambda with Arithmetic Example
   5. Exercise: Lambda with Multiplication
   6. Tips for More Complex Terms
   7. Advanced Challenges
   8. Plutus Term Summary Table

10. Conclusion

11. Glossary of Terms

---

1. Introduction

This guide introduces how to evaluate lambda expressions and applications in Plutus Core using the CEK machine, with a special focus on costing and emitter modes. Understanding these modes is crucial for debugging, optimizing, and ensuring Cardano smart contracts stay within resource limits.

---

2. Costing and Emitter Modes Overview

2.1 Costing Modes Recap

Costing modes determine how resource usage is measured and enforced during script execution:

Mode	Purpose
counting	Tally total resource usage (CPU, memory)
tallying	Tally detailed costs for each operation
restricting	Fail evaluation if a maximum budget is exceeded
restrictingLarge / restrictingEnormous	Allow almost any budget for stress-testing

---

2.2 Emitter Modes Recap

Emitter modes specify what logging information is produced during execution:

Mode	What gets logged
noEmitter	No logs
logEmitter	Basic step logs
logWithTimeEmitter	Step logs with timestamps
logWithBudgetEmitter	Step logs plus budget consumption info

---

3. Running the Demo Script

Below is a demonstration using the expression (λx. x + 1) 3, showcasing different costing and emitter modes:

import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Core.Type (Term(..), Name(..))
import PlutusCore.Default

main = do
  let x = Name () "x" 0
      add = Builtin () (DynBuiltinName "addInteger")
      body = Apply () (Apply () add (Var () x)) (Constant () (Some (ValueOf DefaultUniInteger 1)))
      fun = LamAbs () x body
      arg = Constant () (Some (ValueOf DefaultUniInteger 3))
      applied = Apply () fun arg
      params = defaultCekParameters

  putStrLn "== Counting, No Logging =="
  let (result1, cost1, logs1) = runCek params counting noEmitter applied
  print result1
  print cost1
  print logs1

  putStrLn "\n== Counting, logEmitter =="
  let (result2, cost2, logs2) = runCek params counting logEmitter applied
  print result2
  print cost2
  mapM_ putStrLn logs2

  putStrLn "\n== Counting, logWithBudgetEmitter =="
  let (result3, cost3, logs3) = runCek params counting logWithBudgetEmitter applied
  print result3
  print cost3
  mapM_ putStrLn logs3

  putStrLn "\n== Tallying, logEmitter =="
  let (result4, cost4, logs4) = runCek params tallying logEmitter applied
  print result4
  print cost4
  mapM_ putStrLn logs4

  putStrLn "\n== Restricting with tiny budget (expect failure) =="
  let restrictParams = restricting (ExRestrictingBudget 1 1)
      (result5, cost5, logs5) = runCek params restrictParams logEmitter applied
  print result5
  print cost5
  mapM_ putStrLn logs5

---

4. Understanding Evaluation Results

Below are typical outcomes for various mode combinations:

• Counting + No Logging: Only result and total resource usage (CPU/memory) are shown. No logs.
• Counting + logEmitter: Result, cost, and a step-by-step textual log of the evaluator's process.
• Counting + logWithBudgetEmitter: Same as above, but each log entry includes budget usage so far.
• Tallying + logEmitter: Logs as above, but the cost is a detailed breakdown per operation.
• Restricting (with small budget): Evaluation fails if resource use exceeds the limit (CekEvaluationException).

---

5. Sample Output

== Counting, No Logging ==
Right (Constant () (Some (ValueOf DefaultUniInteger 4)))
ExBudget { cpu = ..., memory = ... }
[]

== Counting, logEmitter ==
Right (Constant () (Some (ValueOf DefaultUniInteger 4)))
ExBudget { cpu = ..., memory = ... }
AppStep: evaluating application ...
BuiltinStep: evaluating builtin addInteger ...
...

== Counting, logWithBudgetEmitter ==
Right (Constant () (Some (ValueOf DefaultUniInteger 4)))
ExBudget { cpu = ..., memory = ... }
AppStep [budget: cpu=5, mem=3]: evaluating application ...
...

== Tallying, logEmitter ==
Right (Constant () (Some (ValueOf DefaultUniInteger 4)))
TallyingSt { addInteger = ExBudget ..., ... }
...

== Restricting with tiny budget (expect failure) ==
Left (CekEvaluationException ...)
ExBudget { cpu = 1, memory = 1 }
...

---

6. Experimentation Guidelines

• Change the emitter mode: Try noEmitter, logEmitter, logWithTimeEmitter, or logWithBudgetEmitter.
• Change the costing mode: Use counting, tallying, or restricting (ExRestrictingBudget cpu mem).
• Change the term: Try more complex terms such as (λx. λy. x * y) 4 5.

---

7. Costing & Logging Summary Table

Costing Mode	Emitter Mode	What you'll see
counting	noEmitter	Result and total cost only
counting	logEmitter	Result, cost, plain step logs
counting	logWithBudgetEmitter	Result, cost, logs with current budget after each step
tallying	logEmitter	Result, detailed cost breakdown, logs
restricting (small)	logEmitter	Likely failure (budget exceeded), logs

---

8. Challenge Exercises

• Adjust the budget: Change the budget in restricting to a larger value so the evaluation succeeds.
• Try other emitters: Use logWithTimeEmitter for timestamped logs.
• Observe inefficient scripts: Use terms with repeated applications and see how resource usage grows.

---

9. Plutus Core Lambda and Application Structure

9.1 Lambda Expressions in Plutus Core

A lambda function in Plutus Core is structured as follows:

LamAbs ann (Name ann Text Unique) (Term Name uni fun ann)

• ann: Annotation (can be ())
• Name: Variable name
• Term: Function body

Example: Identity function (\x -> x) in Plutus Core:

LamAbs () (Name () "x" 0) (Var () (Name () "x" 0))

---

9.2 Application in Plutus Core

Function application in Plutus Core applies a function to an argument:

Apply ann (Term Name uni fun ann) (Term Name uni fun ann)

• First term: function
• Second term: argument

---

9.3 Evaluating: Identity Function Example

Evaluating (λx. x) 42:

import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Core.Type (Term(..), Name(..))
import PlutusCore.Default

main = do
  let x = Name () "x" 0
      identity = LamAbs () x (Var () x)
      arg = Constant () (Some (ValueOf DefaultUniInteger 42))
      applied = Apply () identity arg
      params = defaultCekParameters
      (result, cost, logs) = runCek params counting logEmitter applied
  print result   -- Right (Constant () (Some (ValueOf DefaultUniInteger 42)))
  print cost
  putStrLn "Logs:"
  mapM_ putStrLn logs

---

9.4 Lambda with Arithmetic Example

Evaluating (λx. x + 1) 10:

import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Core.Type (Term(..), Name(..))
import PlutusCore.Default

main = do
  let x = Name () "x" 0
      add = Builtin () (DynBuiltinName "addInteger")
      body = Apply () (Apply () add (Var () x)) (Constant () (Some (ValueOf DefaultUniInteger 1)))
      fun = LamAbs () x body
      arg = Constant () (Some (ValueOf DefaultUniInteger 10))
      applied = Apply () fun arg
      params = defaultCekParameters
      (result, cost, logs) = runCek params counting logEmitter applied
  print result   -- Right (Constant () (Some (ValueOf DefaultUniInteger 11)))
  print cost
  putStrLn "Logs:"
  mapM_ putStrLn logs

---

9.5 Exercise: Lambda with Multiplication

Task: Write and evaluate (λx. x * 2) 7.

Solution:

import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Core.Type (Term(..), Name(..))
import PlutusCore.Default

main = do
  let x = Name () "x" 0
      mul = Builtin () (DynBuiltinName "multiplyInteger")
      body = Apply () (Apply () mul (Var () x)) (Constant () (Some (ValueOf DefaultUniInteger 2)))
      fun = LamAbs () x body
      arg = Constant () (Some (ValueOf DefaultUniInteger 7))
      applied = Apply () fun arg
      params = defaultCekParameters
      (result, cost, logs) = runCek params counting logEmitter applied
  print result   -- Right (Constant () (Some (ValueOf DefaultUniInteger 14)))
  print cost
  putStrLn "Logs:"
  mapM_ putStrLn logs

---

9.6 Tips for More Complex Terms

• Nested Applications: Build up terms incrementally using Apply.
• Multiple Arguments: Use nested lambdas, e.g., (\x y -> x + y) 2 3 as Apply (Apply (LamAbs x (LamAbs y body)) arg1) arg2
• Built-in Functions: Use Builtin () (DynBuiltinName "builtinName") for supported built-ins (e.g., addInteger, multiplyInteger).

---

9.7 Advanced Challenges

• Evaluate (λx. λy. x + y) 5 8 and print the result (should yield 13).
• Evaluate (λx. if x then 1 else 0) True and explore conditional logic.
• Try applying (λx. x) to a boolean value and observe the result.

---

9.8 Plutus Term Summary Table

Plutus Term	Meaning
LamAbs () x (Var () x)	λx. x (identity)
Apply () fun arg	fun applied to arg
Builtin () (DynBuiltinName "addInteger")	Integer addition
Constant () (Some (ValueOf ... value))	Literal constant

---

10. Conclusion

Experimenting with different costing and emitter modes in the CEK machine enables a deep understanding of how Plutus Core terms are evaluated, resource usage is tracked, and logs are generated. This is invaluable for developing, debugging, and optimizing Cardano smart contracts to ensure they perform reliably within resource limits.

---

11. Glossary of Terms

Term	Definition
CEK Machine	An abstract machine used to evaluate Plutus Core terms, tracking cost (CPU, memory) and producing logs.
Costing Mode	Determines how resources are accounted for during script evaluation (e.g., counting, tallying, restricting).
Emitter Mode	Defines the granularity and style of logs emitted during evaluation (e.g., none, simple, with timestamps, with budget info).
Lambda (LamAbs)	A function abstraction in Plutus Core.
Apply	Application of a function to an argument in Plutus Core.
Builtin	Predefined function available in Plutus Core, such as addInteger or multiplyInteger.
Constant	A literal value (e.g., integer, boolean) in Plutus Core.
ExBudget	Data structure representing resource usage (CPU, memory) in script evaluation.
CekEvaluationException	Error thrown when evaluation exceeds a specified resource budget.
DynBuiltinName	Dynamic name referring to a specific built-in function in Plutus Core.
defaultCekParameters	Default configuration parameters for running the CEK machine.

---