lungo documentation

How to call async host operations

Write Lean programs that ask the host to perform operations asynchronously, call them as native async functions in each language, and prove what they do against a model.

In this section

This guide shows how a Lean program asks the application to do something it answers later (read a database, fetch a page, wait for a user) and continues with the answer. Each export returning such a program becomes a native async function in every language, taking a handler that performs the operations. The example is the async-store crate in lungo-rs’s examples directory: programs over a key-value store the host keeps.

Declare the operations

The operations are the constructors of an inductive type; an instance of Lungo.Async.Interface says what each one is answered with, and @[lungo_facility] makes it an async facility. The project requires lungo’s Lean library.

import Lungo

namespace Store

open Lungo.Async

/-- What a program asks of the store. -/
inductive StoreOp where
  | get (key : String)
  | put (key value : String)

@[lungo_facility "store.kv"]
instance storeOps : Interface StoreOp where
  Ret
    | .get _ => Option String
    | .put _ _ => Unit

The operation type and its answers must cross to the host as data (LNG0707):

  • the operation type is an inductive type without parameters or indices, whose fields are data a host can supply (not proofs or types);
  • what each constructor is answered with reduces to a type fixed by the constructor alone, not by its fields (Ret (.get k) cannot depend on k).

@[lungo_facility] checks both when it is given, and lungo checks them again when it reads the program. The constructors are the facility’s operations: an async facility has no @[lungo_operation] externs.

Write the programs

A program is Lungo.Async.Program StoreOp α; Program.perform op asks the host to perform op and returns its answer, in do notation:

/-- Copies the value at `src` to `dst`; whether there was one. -/
def copy (src dst : String) : Program StoreOp Bool := do
  match ← Program.perform (StoreOp.get src) with
  | none => return false
  | some v =>
    let _ ← Program.perform (StoreOp.put dst v)
    return true

Name the constructor in full (StoreOp.get src, not .get src) where the answer is matched on: the answer’s type is known only once the operation is.

An export returning Program Op α is an async function; a program can only be what an export returns, not part of another value (LNG0707).

Call it

Every language calls the export with a handler that has one method per operation, taking the constructor’s fields and returning its answer, asynchronously. The program runs until it asks for an operation, waits for the handler’s answer, and resumes with it; it may ask any number of times, and any number of calls may wait at once, answered in any order.

An error of the handler abandons the program: lungo releases it, and the call fails with the error. So does cancelling the call. A program is resumed at most once per operation it asks.

Rust

The generated trait is named after the operation type; each method returns a future, so an async fn implements it, and the export is an async fn for any executor:

use async_store::StoreOpHandler;

struct Memory {
    data: Mutex<HashMap<String, String>>,
}

impl StoreOpHandler for Memory {
    type Error = Unavailable;

    async fn get(&self, key: String) -> Result<Option<String>, Unavailable> {
        Ok(self.data.lock().unwrap().get(&key).cloned())
    }

    async fn put(&self, key: String, value: String) -> Result<(), Unavailable> {
        self.data.lock().unwrap().insert(key, value);
        Ok(())
    }
}

let copied: bool = async_store::copy(&memory, "a".into(), "c".into()).await?;

A method’s error is what the export returns. Dropping the export’s future releases the program.

Go

The export takes a context.Context and the handler; each method receives the context too:

type memory struct {
	mu   sync.Mutex
	data map[string]string
}

func (m *memory) Get(ctx context.Context, key string) (lungo.Option[string], error) {
	m.mu.Lock()
	defer m.mu.Unlock()
	v, ok := m.data[key]
	return lungo.Option[string]{Value: v, Valid: ok}, nil
}

func (m *memory) Put(ctx context.Context, key, value string) (lungo.Unit, error) {
	m.mu.Lock()
	defer m.mu.Unlock()
	m.data[key] = value
	return lungo.Unit{}, nil
}

copied, err := store.Copy(ctx, m, "a", "c")

A method’s error, a panic, or ctx ending abandons the program: the call returns the error (ctx.Err() when the context ended), or panics again.

Python

The export is a coroutine function; a handler method is a coroutine or returns its answer:

class Memory:
    def __init__(self):
        self.data = {}

    async def get(self, key):
        return self.data.get(key)

    async def put(self, key, value):
        self.data[key] = value

copied = await store.copy(Memory(), "a", "c")

An exception of the handler is raised by the call; cancelling the task (asyncio.CancelledError) abandons the program.

Swift

The handler conforms to <Module><Op>Handler (StoreStoreOpHandler here), a Sendable protocol of async throws methods; the export is async throws:

actor Memory: StoreStoreOpHandler {
    var data: [String: String] = [:]

    func get(_ key: String) async throws -> String? { data[key] }

    func put(_ key: String, _ value: String) async throws -> LungoUnit {
        data[key] = value
        return LungoUnit()
    }
}

let copied = try await copy(Memory(), "a", "c")

An error of the handler is thrown by the call; cancelling the task throws CancellationError.

TypeScript

A handler method returns its answer or a promise of it; the export returns a promise and takes an optional AbortSignal:

const data = new Map();
const memory = {
  get: async (key) => (data.has(key) ? data.get(key) : null),
  put: async (key, value) => { data.set(key, value); return null; },
};
const p = await load();
const copied = await p.copy(memory, "a", "c", { signal: AbortSignal.timeout(5000) });

A rejection of the handler rejects the call; the signal aborting rejects it with the signal’s reason.

C

The export returns the program’s first step; the host answers each operation with lungo_resume, until the step is LUNGO_STEP_DONE:

lungo_step step;
lungo_error *error = NULL;
if (store_copy(src, dst, &step, &error) != LUNGO_OK) { /* malformed arguments */ }
while (step.kind == LUNGO_STEP_CALL) {
    lungo_value *answer;
    if (lungo_value_ctor_index(step.value) == STORE_STORE_OP_GET) {
        answer = lookup(store_store_op_get_key(step.value)); /* an Option String */
    } else {
        write(store_store_op_put_key(step.value), store_store_op_put_value(step.value));
        answer = lungo_value_unit();
    }
    uint64_t resumption = step.resumption;
    lungo_step_clear(&step);
    int32_t status = lungo_resume(resumption, answer, &step, &error);
    lungo_value_free(answer);
    if (status != LUNGO_OK) { /* LUNGO_MALFORMED: an answer of another type */ }
}
bool copied = lungo_value_get_bool(step.value);
lungo_step_clear(&step);

step.value is the operation asked (a value of the operation type) or the program’s value; the answer is borrowed. An answer of another type is refused with LUNGO_MALFORMED and gives the program up; resuming a resumption again, or one given up, is LUNGO_STALE. To give a program up, call lungo_async_cancel(step.resumption).

Count what waits

Each language reports how many programs are waiting for an answer, which is zero once every call has settled: lungo.Outstanding() in Go, lungo_py.outstanding() in Python, lungoOutstanding() in Swift, the program’s outstanding() in TypeScript (each loaded program has its own), and lungo_async_outstanding() in C. In Rust a waiting program is held by the future that waits for it.

Prove what a program does

A program is data, so Lean can run it against a model of the host. Program.run interprets it with any handler in any monad; here a store is a function from keys to values, and the model answers in StateM:

abbrev Contents := String → Option String

private def Contents.set (contents : Contents) (key value : String) : Contents :=
  fun k => if k = key then some value else contents k

@[lungo_spec "lungo.model"]
noncomputable def Model : (op : StoreOp) → StateM Contents (Interface.Ret op)
  | .get key => fun s => (s key, s)
  | .put key value => fun s => ((), s.set key value)

@[lungo_claim "lungo.law" subject copy spec Model]
theorem copy_model (s : Contents) (src dst : String) :
    (Program.run Model (copy src dst)).run s =
      match s src with
      | none => (false, s)
      | some v => (true, s.set dst v) := by
  cases h : s src <;> simp [copy, Program.perform, Program.run, Model, h, bind, Program.bind,
    StateT.run, StateT.bind, pure, StateT.pure]

Contents.set is private: it serves the model and the claims, and a public definition would be exported to every binding, where a function over a function type is of no use. The claim says what copy does to every store kept as the model keeps it. To say it holds of the host’s store, state that as an assumption (see how to declare facilities and assumptions). Program.Admits and Program.trace relate a program to the operations it asks and the answers it is given, for claims about the exchanges themselves (see how to state claims about exports).