Dafny to JavaScript type conversion reference guide

Dafny compiles to JavaScript, but the two type systems do not map one-to-one. Dafny integers become BigNumber objects, strings become character sequences, and algebraic datatypes use constructor and destructor naming conventions. This page documents every type boundary you will encounter when writing app-extras.js wrappers or calling generated code directly.

Loading Dafny code

Before calling any Dafny-generated functions, you must load the compiled .cjs bundle and configure BigNumber.

Client (Vite)
Server (Node.js)

import BigNumber from 'bignumber.js';
BigNumber.config({ MODULO_MODE: BigNumber.EUCLID });

import myAppCode from './MyApp.cjs?raw';

const require = (mod) => {
  if (mod === 'bignumber.js') return BigNumber;
  throw new Error(`Unknown module: ${mod}`);
};

const initDafny = new Function('require', `
  ${myAppCode}
  return { _dafny, MyAppDomain, AppCore };
`);

const { _dafny, AppCore } = initDafny(require);

import { readFileSync } from 'fs';
import { fileURLToPath } from 'url';
import { dirname, join } from 'path';
import BigNumber from 'bignumber.js';

BigNumber.config({ MODULO_MODE: BigNumber.EUCLID });

const __filename = fileURLToPath(import.meta.url);
const __dirname = dirname(__filename);
const myAppCode = readFileSync(join(__dirname, 'MyApp.cjs'), 'utf-8');

const require = (mod) => {
  if (mod === 'bignumber.js') return BigNumber;
  throw new Error(`Unknown module: ${mod}`);
};

const initDafny = new Function('require', `
  ${myAppCode}
  return { _dafny, MyAppDomain, AppCore };
`);

const { _dafny, AppCore } = initDafny(require);

BigNumber.config({ MODULO_MODE: BigNumber.EUCLID }) must be called before any Dafny code runs. Dafny’s modulo semantics for negative numbers differ from JavaScript’s default, and skipping this line causes incorrect arithmetic.

Calling module functions

All Dafny top-level functions are exposed under Module.__default:

AppCore.__default.Init()
AppCore.__default.Dispatch(state, action)

Type mappings

Numbers (BigNumber)

Dafny integers compile to BigNumber objects from the bignumber.js library.

Direction	Pattern
JS → Dafny	`new BigNumber(42)`
Dafny → JS	`bn.toNumber()`
Zero constant	`_dafny.ZERO`

// JS → Dafny
const dafnyInt = new BigNumber(42);

// Dafny → JS
const jsNumber = dafnyInt.toNumber();

// The zero constant from the _dafny runtime
const zero = _dafny.ZERO;

Strings (`seq<char>`)

Dafny string is a sequence of characters, not a JavaScript string.

Direction	Pattern
JS → Dafny	`_dafny.Seq.UnicodeFromString("hello")`
Dafny → JS (preferred)	`seq.toVerbatimString(false)`
Dafny → JS (manual)	`Array.from(seq).join('')`

// JS → Dafny
const dafnyStr = _dafny.Seq.UnicodeFromString("hello");

// Dafny → JS
const jsStr = dafnyStr.toVerbatimString(false);

Sequences (`seq<T>`)

Direction	Pattern
JS array → Dafny seq	`_dafny.Seq.of(...jsArray)`
Dafny seq → JS array	Index loop over `seq.length`

// JS array → Dafny seq
const dafnySeq = _dafny.Seq.of(...jsArray);

// Dafny seq → JS array
const arr = [];
for (let i = 0; i < seq.length; i++) {
  arr.push(seq[i]);
}

Sets (`set<T>`)

Direction	Pattern
JS array → Dafny set	`_dafny.Set.fromElements(...jsArray)`
Dafny set → JS array	`Array.from(set.Elements)`

// JS array → Dafny set
const dafnySet = _dafny.Set.fromElements(...jsArray);

// Dafny set → JS array
const jsArray = Array.from(dafnySet.Elements);

Maps (`map<K, V>`)

Dafny maps are immutable. Use .update() to return a new map with an added entry.

Operation	Pattern
Empty map	`_dafny.Map.Empty`
Add entry	`map = map.update(key, value)`
Check key	`map.contains(key)`
Get value	`map.get(key)`
Iterate keys	`for (const key of map.Keys.Elements)`
Iterate pairs	`for (let i = 0; i < map.length; i++)`

// Create and populate a map
let m = _dafny.Map.Empty;
m = m.update(_dafny.Seq.UnicodeFromString("alice"), new BigNumber(100));

// Check and retrieve
if (m.contains(_dafny.Seq.UnicodeFromString("alice"))) {
  const balance = m.get(_dafny.Seq.UnicodeFromString("alice"));
}

// Iterate keys
for (const key of m.Keys.Elements) {
  const value = m.get(key);
  console.log(key.toVerbatimString(false), value.toNumber());
}

// Iterate key-value pairs
for (let i = 0; i < m.length; i++) {
  const [key, val] = m[i];
}

Datatypes

Dafny algebraic datatypes use a consistent naming convention for constructors, variant checks, and field accessors.

Operation	Pattern
Construct a variant	`Module.Type.create_Variant(args...)`
Check variant	`value.is_Variant`
Access a field	`value.dtor_fieldName`

// Constructors
const incAction = Module.Action.create_Inc();
const moveAction = Module.Action.create_Move(
  new BigNumber(3),
  _dafny.Seq.UnicodeFromString("done")
);

// Variant checks
if (action.is_Inc) {
  // handle increment
}

// Field access
const title = card.dtor_title.toVerbatimString(false);
const column = card.dtor_column.toVerbatimString(false);

Dafny reserved words used as field names are escaped with the dtor_ prefix. For example, a Dafny field named from becomes dtor_from in JavaScript:

const sender = delegation.dtor_from.toVerbatimString(false);

Tuple returns

Dafny functions that return tuples destructure directly in JavaScript:

const [newState, response] = AppCore.__default.Dispatch(serverState, action);
serverState = newState;

Result types (`Result<T, E>`)

If your Dafny domain defines a Result type, the compiled JavaScript exposes it with is_Ok, dtor_value, and dtor_error:

const result = AppCore.__default.TryStep(model, action);

if (result.is_Ok) {
  const newModel = result.dtor_value;
  // proceed with newModel
} else {
  const error = result.dtor_error;
  // handle error
}

The app-extras.js pattern

When you need to customize the generated API — for example, to accept plain JavaScript types instead of Dafny types — create app-extras.js that wraps app.js:

import GeneratedApp from './app.js';

const { _dafny, MyAppCore } = GeneratedApp._internal;

const App = {
  ...GeneratedApp, // inherit everything from generated

  // Override or add methods below
  Init: (members) => {
    const memberSeq = _dafny.Seq.of(
      ...members.map(m => _dafny.Seq.UnicodeFromString(m))
    );
    const result = MyAppCore.__default.Init(memberSeq);
    if (result.is_Ok) {
      return { ok: true, model: result.dtor_value };
    } else {
      return { ok: false, error: GeneratedApp.errToJson(result.dtor_error) };
    }
  },
};

export default App;

Always call GeneratedApp functions rather than AppCore.__default directly inside app-extras.js. The generated app.js layer handles JS → Dafny type conversions. Calling AppCore.__default directly with raw JavaScript strings will fail because Dafny expects seq<char>, not a JS string.

Common customization patterns

Derive parameters automatically:

// Generated: MakeExpense(paidBy, amount, shares, shareKeys)
// Simplified: MakeExpense(paidBy, amount, shares)
MakeExpense: (paidBy, amountCents, shares) => {
  const shareKeys = Object.keys(shares);
  return GeneratedApp.MakeExpense(paidBy, amountCents, shares, shareKeys);
},

Provide object-style enum access:

// Instead of: App.Vibrant()
// Allow:      App.Mood.Vibrant
Mood: {
  Vibrant: ColorWheelSpec.Mood.create_Vibrant(),
  Pastel:  ColorWheelSpec.Mood.create_Pastel(),
},

Return all map entries instead of a single lookup:

GetDelegations: (m) => {
  const delegations = m.dtor_delegations;
  const result = [];
  for (const key of delegations.Keys.Elements) {
    const deleg = delegations.get(key);
    result.push({
      id:   key.toNumber(),
      from: deleg.dtor_from.toVerbatimString(false),
      to:   deleg.dtor_to.toVerbatimString(false),
    });
  }
  return result;
},

JSON serialization

The generated app.js includes toJson/fromJson for all datatypes:

// Serialize for network transport
const json = App.actionToJson(action);
const action = App.actionFromJson(json);

// Full model serialization
const modelJson = App.modelToJson(model);
const model = App.modelFromJson(modelJson);

dafny2js tool

Generate JavaScript API wrappers automatically from your Dafny code.

app-extras pattern

Full guide to customizing the generated API without modifying generated code.

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Dafny to JavaScript type conversion reference guide

Loading Dafny code

Calling module functions

Type mappings

Numbers (BigNumber)

Strings (`seq<char>`)

Sequences (`seq<T>`)

Sets (`set<T>`)

Maps (`map<K, V>`)

Datatypes

Tuple returns

Result types (`Result<T, E>`)

The app-extras.js pattern

Common customization patterns

JSON serialization

dafny2js tool

app-extras pattern

Build docs developers (and LLMs) love

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Documentation Index

​Loading Dafny code

​Calling module functions

​Type mappings

​Numbers (BigNumber)

​Strings (seq<char>)

​Sequences (seq<T>)

​Sets (set<T>)

​Maps (map<K, V>)

​Datatypes

​Tuple returns

​Result types (Result<T, E>)

​The app-extras.js pattern

​Common customization patterns

​JSON serialization

dafny2js tool

app-extras pattern

Build docs developers (and LLMs) love

Loading Dafny code

Calling module functions

Type mappings

Numbers (BigNumber)

Strings (`seq<char>`)

Sequences (`seq<T>`)

Sets (`set<T>`)

Maps (`map<K, V>`)

Datatypes

Tuple returns

Result types (`Result<T, E>`)

The app-extras.js pattern

Common customization patterns

JSON serialization