How to declare facilities and assumptions

This guide shows how a Lean program declares what it needs from the application that runs it, a facility, and what its claims assume of the application’s implementation, an assumption. The example is the clock crate in lungo-rs’s examples directory: deadlines computed on a clock the host provides.

Declare the facility

A facility is a declaration with @[lungo_facility "<identifier>"], the anchor its operations and assumptions name; its operations are @[extern] declarations marked @[lungo_operation <facility>]. The project requires lungo’s Lean library.

import Lungo

namespace Timing

/-- The host's clock. -/
@[lungo_facility "timing.clock"]
structure Clock

/-- Ticks of the host's clock per second. -/
@[extern "timing_ticks_per_second", lungo_operation Clock]
opaque ticksPerSecond (u : Unit) : Nat

/-- The time now, in ticks of the host's clock. -/
@[extern "timing_now", lungo_operation Clock]
opaque now (u : Unit) : IO Nat

def toTicks (seconds : Nat) : Nat := seconds * ticksPerSecond ()

def toSeconds (ticks : Nat) : Nat := ticks / ticksPerSecond ()

def deadlineIn (seconds : Nat) : IO Nat := do
  return (← now ()) + toTicks seconds

end Timing

The identifier is a namespaced string of your own (timing.clock; the lungo namespace is lungo’s), unique in the program (LNG0705); its last segment names the facility in each language (Clock, set_clock, clock). @[extern …] comes before @[lungo_operation …] on the same declaration. An operation whose symbol the lungo runtime or a Lean @[export] already implements is refused (LNG0706), and so is an extern that is no facility’s operation and that nothing implements (LNG0401).

Every operation of a facility the program’s modules declare is part of the program’s interface, whether or not the program calls it.

State what the claims assume

What Lean cannot check about the host, a claim can assume. An assumption is a proposition (or a family of them, or a class in Prop) about the facility’s operations, marked @[lungo_assumption <facility>]:

/-- What the claims assume of the host's clock: it ticks. -/
@[lungo_assumption Clock]
def Ticks : Prop := 0 < ticksPerSecond ()

@[lungo_claim "lungo.roundtrip" subject toTicks toSeconds]
theorem toSeconds_toTicks (h : Ticks) (seconds : Nat) : toSeconds (toTicks seconds) = seconds :=
  Nat.mul_div_cancel seconds h

The claim is proved, under the hypothesis Ticks; lungo finds the assumptions among a claim’s hypotheses and reports the claim as conditional on them, and each export as resting on the assumptions of its claims and needing the facilities it calls:

$ lungo assurance Timing.toSeconds
Timing.toSeconds
  == Claims ==
    [proved] lungo.roundtrip Timing.toSeconds_toTicks — assuming Timing.Ticks
  == Trust ==
    (none)
  == Assumptions ==
    [assumed] Timing.Ticks : 0 < Timing.ticksPerSecond () (of Timing.Clock)
  == Facilities ==
    timing.clock (Timing.Clock)

Making the assumption true is the host’s part. On a host whose clock does not tick, the exports still run, and compute what the claim does not promise (toSeconds (toTicks 7) is 0); the C test of the clock example runs both hosts.

Implement it

Each generated package has, per facility, an interface (or protocol) with one method per operation, named after the Lean declaration, and an installer. An IO operation fails with the language’s IO error; an operation that is not IO or EIO must not fail: its failure terminates the program.

An operation with a pure Lean type must behave as a pure function: Lean’s compiler may evaluate ticksPerSecond () once and keep the value, so a host that answers differently later is not heard. Something that changes, such as the time, is an IO operation.

Install every facility before the program’s first call.

Rust

A Rust function implements each operation, named by its symbol in build.rs:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure()
        .rust_extern("timing_ticks_per_second", "crate::host::ticks_per_second")
        .rust_extern("timing_now", "crate::host::now")
        .compile_lean("lean")
}

or in lungo.toml:

[rust.rust-externs]
timing_ticks_per_second = "crate::host::ticks_per_second"
timing_now = "crate::host::now"

pub mod host {
    use lungo::{IoError, Nat};

    pub fn ticks_per_second(_u: ()) -> Nat {
        Nat::from(1000u64)
    }

    pub fn now(_u: ()) -> Result<Nat, IoError> {
        Ok(Nat::from(read_clock()))
    }
}

A reachable operation without a mapping fails the build with LNG0401; a mapping of an extern that is no facility’s operation, with LNG0706. See also how to call Rust functions from Lean.

Go

type clock struct{}

func (clock) Now(u lungo.Unit) (*big.Int, error)            { return big.NewInt(readClock()), nil }
func (clock) TicksPerSecond(u lungo.Unit) (*big.Int, error) { return big.NewInt(1000), nil }

timing.SetClock(clock{})

Python

class Clock:
    def now(self, u):
        return read_clock()

    def ticks_per_second(self, u):
        return 1000

timing.set_clock(Clock())

Swift

final class Clock: TimingClock {
    func now(_ u: LungoUnit) throws -> LungoNat { LungoNat(readClock()) }
    func ticksPerSecond(_ u: LungoUnit) throws -> LungoNat { 1000 }
}

setClock(Clock())

TypeScript

The facilities are given to load, by name:

const p = await load({
  facilities: {
    clock: { now: () => readClock(), ticksPerSecond: () => 1000n },
  },
});

C

static int32_t now(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error) {
    *result = lungo_value_nat(read_clock());
    return LUNGO_OK;
}

static int32_t ticks_per_second(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result,
                                lungo_error **error) {
    *result = lungo_value_nat(1000);
    return LUNGO_OK;
}

timing_implement_clock_now(now, NULL, NULL);
timing_implement_clock_ticks_per_second(ticks_per_second, NULL, NULL);

An IO operation fails with *error = lungo_error_io("…") and return LUNGO_FAILED;.

A facility not installed

A call before every facility is installed fails, naming the facility and one of its operations:

Forbid an assumption

A project can refuse claims that rest on an assumption, or on any assumption of a facility, and exports that call a facility’s operations:

# lungo.toml
[assurance]
forbid-assumptions = ["Timing.Ticks"]

(Builder::forbid_assumption("Timing.Ticks")). A proved claim taking Timing.Ticks as a hypothesis then fails the build with LNG0603; naming the facility ("Timing.Clock") also refuses every export that calls one of its operations. A name that is neither an assumption nor a facility of the program is a configuration error.

See what each export needs

lungo assurance --facility timing.clock lists the exports needing the facility (by identifier or Lean name), --assumption Timing.Ticks those whose claims assume it. Every package carries the same in its assurance document, in the facility records (id, form, operations, assumptions) and each export’s facilities and assumptions (see the assurance document). For operations the host answers asynchronously, see how to call async host operations.