Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/metareflection/dafny-replay/llms.txt

Use this file to discover all available pages before exploring further.

The file that dafny2js generates is a faithful, mechanical translation of your AppCore module into JavaScript. It is correct and complete, but it reflects Dafny’s type system rather than the idioms that JavaScript callers expect. app-extras.js is the sanctioned place to add that translation layer: it imports GeneratedApp, extends it with convenience methods, and re-exports the result as the App object your components use. Because it is a separate file, it survives regeneration of app.js intact.

​
When to use app-extras.js

Use app-extras.js when you need to:
  • Wrap Result<T, E> return types into {ok, model} objects that are easier to branch on in JavaScript
  • Derive parameters automatically so callers pass fewer arguments
  • Expose enum values as object properties instead of zero-argument constructor calls
  • Flatten Dafny maps into JavaScript arrays for easier iteration
  • Accept serialized JSON on the boundary with a server or edge function

​
The base pattern

Create src/dafny/app-extras.js in your app: 
import GeneratedApp from './app.js';

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

  // Override or add methods here
};

export default App;
Then import from app-extras.js in your components instead of app.js: 
// Before
import App from './dafny/app.js'

// After
import App from './dafny/app-extras.js'
Always spread ...GeneratedApp first and override selectively. Never rebuild the entire object from scratch: you will miss converter functions (actionToJson, historyToJson, etc.) and the _internal accessor needed for advanced customizations.

​
Pattern 1: Wrap Result types

Dafny functions that can fail return Result<T, E> values. The raw Dafny runtime represents these as objects with is_Ok / is_Err discriminants and dtor_value / dtor_error destructors. In JavaScript, it is more idiomatic to return {ok: true, model: ...} or {ok: false, error: ...}. 
import GeneratedApp from './app.js';

const { _dafny, ClearSplitAppCore } = GeneratedApp._internal;

const App = {
  ...GeneratedApp,

  Init: (members) => {
    const memberSeq = _dafny.Seq.of(
      ...members.map(m => _dafny.Seq.UnicodeFromString(m))
    );
    const result = ClearSplitAppCore.__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;
In the component, the caller can now branch without knowing Dafny’s discriminant naming: 
const result = App.Init(['Alice', 'Bob', 'Carol']);
if (result.ok) {
  setH(result.model);
} else {
  console.error(result.error);
}

​
Pattern 2: Derive parameters automatically

Some AppCore functions take a parameter that is always derivable from another argument. For example, if MakeExpense requires both a shares object and its shareKeys array, the caller should not have to supply both: 
const App = {
  ...GeneratedApp,

  // Generated signature: MakeExpense(paidBy, amountCents, shares, shareKeys)
  // Simplified signature: MakeExpense(paidBy, amountCents, shares)
  MakeExpense: (paidBy, amountCents, shares) => {
    const shareKeys = Object.keys(shares);
    return GeneratedApp.MakeExpense(paidBy, amountCents, shares, shareKeys);
  },
};
The key discipline here: delegate immediately to GeneratedApp.MakeExpense. The generated function handles converting paidBy from a JavaScript string to a Dafny seq<char>, converting amountCents to a BigNumber, and converting each share value. If you call AppCore.__default.MakeExpense directly, those conversions are bypassed.

​
Pattern 3: Object-style enum access

Dafny constructors with no arguments compile to zero-argument factory functions: App.Vibrant(). When you have many enum variants, the parentheses become noise and the pattern is unfamiliar to JavaScript developers. You can expose an object-style accessor: 
const { ColorWheelSpec } = GeneratedApp._internal;

const App = {
  ...GeneratedApp,

  // Instead of: App.Vibrant()
  // Allow:      App.Mood.Vibrant
  Mood: {
    Vibrant: ColorWheelSpec.Mood.create_Vibrant(),
    Pastel:  ColorWheelSpec.Mood.create_Pastel(),
    Neon:    ColorWheelSpec.Mood.create_Neon(),
    Custom:  ColorWheelSpec.Mood.create_Custom(),
  },
};
The values are created once at module load time and reused. Dafny datatype constructors are value types — equality is structural — so sharing instances is safe.

​
Pattern 4: Return all map entries

Generated accessors typically look up a single entry in a Dafny map. If you need to expose the entire map as a JavaScript array, iterate the map’s Keys.Elements: 
const App = {
  ...GeneratedApp,

  // Generated: GetDelegation(m, id) → single delegation
  // Extended:  GetDelegations(m)    → all delegations as array
  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: Array.from(deleg.dtor_from).join(''),
        to:   Array.from(deleg.dtor_to).join(''),
      });
    }
    return result;
  },
};
Dafny map objects expose their keys through map.Keys.Elements (an iterable) and values through map.get(key). Dafny strings (seq<char>) can be converted to JavaScript strings with Array.from(seq).join('') or .toVerbatimString(false).

​
Pattern 5: Accept JSON for server communication

When your app communicates with a server or edge function, it is convenient to pass and receive plain JSON rather than Dafny runtime objects. Use the generated modelFromJson and modelToJson converters inside a wrapper: 
const App = {
  ...GeneratedApp,

  // Accept a version number and a plain-JSON model snapshot
  // to reconstruct client state after reconnecting
  InitClient: (version, modelJson) => {
    const model = GeneratedApp.modelFromJson(modelJson);
    return GeneratedApp.MakeClientState(version, model, []);
  },

  // Accept an action as JSON (e.g., received from the server)
  DispatchFromJson: (h, actionJson) => {
    const action = GeneratedApp.actionFromJson(actionJson);
    return GeneratedApp.Dispatch(h, action);
  },
};
This pattern is especially useful for Dafny applications that use the Authority or Multi-Collaboration kernels, where client and server exchange serialized actions and model snapshots.

​
Why always delegate to GeneratedApp

The generated app.js inserts type conversions at every boundary:
  • JavaScript strings → _dafny.Seq.UnicodeFromString(s) (Dafny seq<char>)
  • JavaScript numbers → new BigNumber(n) (Dafny int)
  • JavaScript arrays → _dafny.Seq.of(...arr) (Dafny seq<T>)
If you call AppCore.__default.SomeFunction directly and pass a raw JavaScript string, Dafny will receive a string where it expects a sequence of characters, and the result will be silently wrong or throw at runtime. Delegating to GeneratedApp functions keeps all those conversions in the generated code where they are tested and correct: 
// Correct: type conversion happens inside GeneratedApp.MakeExpense
MakeExpense: (paidBy, amount, shares) => {
  return GeneratedApp.MakeExpense(paidBy, amount, shares, Object.keys(shares));
},

// Incorrect: paidBy is passed as a raw JS string to Dafny
MakeExpense: (paidBy, amount, shares) => {
  return AppCore.__default.MakeExpense(
    paidBy,   // ← raw JS string, Dafny expects seq<char>
    ...
  );
},
If you need a function that AppCore does not expose, add it to your Dafny AppCore module and regenerate app.js. This keeps the conversion logic in the generated layer rather than in app-extras.js.

dafny2js tool

Understand what the generated app.js contains and how to regenerate it.

React integration

Wire the App object from app-extras.js into React state and JSX.

Build docs developers (and LLMs) love

Get started for freeTalk to us