Printing and Debugging

Sector9 provides Debug.print for development-time output and debug_show for converting values to text. In verification, debug output itself is erased, but argument expressions are still checked and evaluated for their normal proof obligations.

The Debug Module

Import the Debug module to access printing functions:

import Debug "mo:core/Debug";

Debug.print

Prints text to the output stream:

Debug.print("Hello, world!");
Debug.print("Counter value: " # debug_show(42));

On the Internet Computer, output goes to the canister log. In the interpreter or standalone Wasm, output goes to standard out.

trap

Terminates execution if a condition is true:

trap (amount > balance)("Insufficient funds");
trap (user == null)("User not found");

When the condition evaluates to true, execution halts and the caller's await receives an Error with code #canister_error. For verification, trap also marks that code path as unreachable, so the verifier must prove execution cannot continue when the condition holds.

The debug_show Prefix

Convert any value to its text representation using debug_show:

let n : Nat = 42;
let pair = (1, "hello");
let record = { x = 10; y = 20 };

Debug.print(debug_show(n));       // "42"
Debug.print(debug_show(pair));    // "(1, \"hello\")"
Debug.print(debug_show(record));  // "{x = 10; y = 20}"

The debug_show prefix is purely computational and produces no side effects. It works with any type.

Debug Blocks

Wrap debug code in debug { } blocks to enable conditional compilation:

debug {
  Debug.print("This only runs in debug mode");
};

Debug blocks must return (). This is invalid:

debug { 42 };  // ERROR: expected (), got Nat

Release Mode

Compile with --release to strip all debug blocks:

sector9 -c --release file.sr9

In release mode:

• debug { } blocks are completely erased
• Debug.print calls outside debug blocks still execute

Use debug blocks for development output that should not appear in production.

Debug vs Verification Assertions

Debug output and verification assertions serve different purposes:

Feature	Purpose	Runtime Effect	Verification Effect
Debug.print	Development output	Prints text	Print erased; arguments still checked
debug_show	Value to text	Computes text	Modeled as a deterministic value for its argument type
debug { }	Conditional debug code	Runs in debug mode	Body expressions are still checked and modeled where evaluated
assert	Proof checkpoint	None (erased)	Must prove true
runtime:assert	Safety check	Traps if false	Must prove true

Debug output is erased during Viper translation. The expressions you pass to it still matter: bounds checks, calls, debug_show arguments, and other evaluated subexpressions keep their normal proof obligations. A debug { ... } block is not a way to hide unsafe code from the verifier.

Primitive Print Functions

The core Debug module wraps primitive print operations. Direct primitive imports are mainly for the core library and low-level tests:

import Prim "mo:⛔";

Prim.debugPrint("text");           // Print text
Prim.debugPrintNat(42);            // Print Nat
Prim.debugPrintInt(-5);            // Print Int
Prim.debugPrintChar('x');          // Print Char

Prefer Debug.print with debug_show for most uses.

Common Patterns

Tracing Execution

public func transfer(from : Principal, to : Principal, amount : Nat) : async Bool
  modifies balances
{
  debug {
    Debug.print("transfer: " # debug_show({ from; to; amount }));
  };

  // ... implementation
}

State Inspection

public func debugState() : async () {
  Debug.print("balance = " # debug_show(balance));
  Debug.print("counter = " # debug_show(counter));
  Debug.print("config = " # debug_show(config));
}

Upgrade Debugging

system func preupgrade() {
  Debug.print("preupgrade: saving state");
  Debug.print("items = " # debug_show(Array.size(items)));
}

system func postupgrade() {
  Debug.print("postupgrade: state restored");
}

Memory Metrics

import Prim "mo:⛔";

Debug.print(debug_show({
  memory = Prim.rts_memory_size() / (1024 * 1024);
  heap = Prim.rts_heap_size() / (1024 * 1024);
}));

Restrictions

No Debug in Pure Functions

Pure functions cannot use Debug.print because it performs I/O:

pure func square(n : Nat) : Nat {
  Debug.print("computing");  // ERROR: side effect in pure function
  n * n
}

No Debug in Lemmas

Lemmas are proof-only and cannot contain runtime code:

lemma func addCommutes(a : Nat, b : Nat) : ()
  ensures a + b == b + a
{
  Debug.print("proving");  // ERROR: not allowed in lemma
}

Debug Blocks Must Return Unit

Debug blocks must have type ():

debug { Debug.print("ok") };  // OK: returns ()
debug { 42 };                  // ERROR: returns Nat
debug { if (x > 0) { } };     // OK: if without else returns ()

When to Use Debugging vs Verification

Use Debug.print When

• Exploring code behavior during development
• Tracing execution flow to understand logic
• Inspecting values at specific program points
• Debugging upgrade migrations

Use Verification Assertions When

• Documenting invariants that must always hold
• Proving specified properties for symbolic inputs
• Catching bugs before deployment
• Expressing safety-critical properties

Debug output helps you understand what your code does. Verification checks that the code satisfies its written specifications.

Best Practices

Wrap Development Output in Debug Blocks

// GOOD: stripped in release
debug { Debug.print("debug info"); };

// AVOID: remains in production
Debug.print("debug info");

Use Structured Output

// GOOD: structured and readable
Debug.print(debug_show({ operation = "transfer"; from; to; amount }));

// AVOID: hard to parse
Debug.print("transfer from " # debug_show(from) # " to " # debug_show(to));

Remove Debug Code Before Verification

Debug output adds noise without proof benefit. Wrap it before compiling production builds; the verifier still checks the wrapped expressions when they remain in the verified source:

public func compute(n : Nat) : async Nat
  ensures result == n * 2
{
  // Debug output doesn't affect verification,
  // but wrapping keeps code clean for production
  debug { Debug.print("computing " # debug_show(n)); };
  n * 2
}

Summary

• Debug.print outputs text for development; the print is erased in Viper, but its arguments are still checked
• debug_show converts values to text representation and is modeled deterministically in proofs
• debug { } blocks compile conditionally; stripped with --release, but still checked by the verifier while present in source
• Debug utilities are erased during Viper translation
• Pure functions and lemmas cannot use debug output
• Use verification assertions for correctness proofs, debug output for development exploration
• Wrap development output in debug blocks for clean production builds