Come dichiarare facility e assunzioni

Questa guida mostra come un programma Lean dichiara ciò di cui ha bisogno dall’applicazione che lo esegue, una facility, e ciò che i suoi claim assumono dell’implementazione dell’applicazione, un’assunzione. L’esempio è il crate clock nella directory examples di lungo-rs: scadenze calcolate su un orologio fornito dall’host.

Dichiara la facility

Una facility è una dichiarazione con @[lungo_facility "<identificatore>"], l’ancora che le sue operazioni e assunzioni nominano; le sue operazioni sono dichiarazioni @[extern] marcate con @[lungo_operation <facility>]. Il progetto richiede la libreria Lean di lungo.

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

L’identificatore è una stringa con spazio dei nomi tuo (timing.clock; lo spazio dei nomi lungo è di lungo), unica nel programma (LNG0705); il suo ultimo segmento dà il nome alla facility in ogni linguaggio (Clock, set_clock, clock). @[extern …] precede @[lungo_operation …] sulla stessa dichiarazione. Un’operazione il cui simbolo è già implementato dal runtime di lungo o da un @[export] Lean viene rifiutata (LNG0706), e così un extern che non è operazione di alcuna facility e che nessuno implementa (LNG0401).

Ogni operazione di una facility dichiarata dai moduli del programma fa parte dell’interfaccia del programma, che il programma la chiami o no.

Enuncia ciò che i claim assumono

Ciò che Lean non può verificare dell’host, un claim può assumerlo. Un’assunzione è una proposizione (o una famiglia di proposizioni, o una classe in Prop) sulle operazioni della facility, marcata con @[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

Il claim è dimostrato, sotto l’ipotesi Ticks; lungo trova le assunzioni fra le ipotesi di un claim e lo riporta come condizionato a esse, e ogni export come poggiante sulle assunzioni dei suoi claim e bisognoso delle facility che chiama:

$ 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)

Rendere vera l’assunzione spetta all’host. Su un host il cui orologio non avanza gli export funzionano comunque, e calcolano ciò che il claim non promette (toSeconds (toTicks 7) vale 0); il test C dell’esempio clock esegue entrambi gli host.

Implementala

Ogni pacchetto generato ha, per ogni facility, un’interfaccia (o protocollo) con un metodo per operazione, con il nome della dichiarazione Lean, e una funzione che la installa. Un’operazione IO fallisce con l’errore di IO del linguaggio; un’operazione che non è IO né EIO non deve fallire: un suo fallimento termina il programma.

Un’operazione con un tipo Lean puro deve comportarsi come una funzione pura: il compilatore di Lean può valutare ticksPerSecond () una volta e conservarne il valore, quindi un host che in seguito risponde diversamente non viene ascoltato. Ciò che cambia, come l’ora, è un’operazione IO.

Installa ogni facility prima della prima chiamata del programma.

Rust

Una funzione Rust implementa ogni operazione, indicata per simbolo 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")
}

oppure 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()))
    }
}

Un’operazione raggiungibile senza associazione fa fallire la build con LNG0401; l’associazione di un extern che non è operazione di alcuna facility, con LNG0706. Vedi anche come chiamare funzioni Rust da 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

Le facility si passano a load, per nome:

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);

Un’operazione IO fallisce con *error = lungo_error_io("…") e return LUNGO_FAILED;.

Una facility non installata

Una chiamata prima che ogni facility sia installata fallisce, nominando la facility e una delle sue operazioni:

Vieta un’assunzione

Un progetto può rifiutare i claim che poggiano su un’assunzione, o su qualsiasi assunzione di una facility, e gli export che chiamano le operazioni di una facility:

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

(Builder::forbid_assumption("Timing.Ticks")). Un claim dimostrato che prende Timing.Ticks come ipotesi fa allora fallire la build con LNG0603; nominare la facility ("Timing.Clock") rifiuta anche ogni export che chiama una delle sue operazioni. Un nome che non è né un’assunzione né una facility del programma è un errore di configurazione.

Vedi di che cosa ha bisogno ogni export

lungo assurance --facility timing.clock elenca gli export che hanno bisogno della facility (per identificatore o nome Lean), --assumption Timing.Ticks quelli i cui claim la assumono. Ogni pacchetto porta le stesse informazioni nel suo documento di garanzia, nei record delle facility (id, form, operations, assumptions) e nei campi facilities e assumptions di ogni export (vedi il documento di garanzia). Per le operazioni a cui l’host risponde in modo asincrono, vedi come chiamare operazioni asincrone dell’host.