Effects and deliveries

A Vishy program has no input or output of its own: no file, no clock it did not declare, no network. The world comes in and goes out through two declared openings. An effect is a function written in Rust that a flow calls, for a fact the program cannot compute. A delivery says where an emitted event goes once the flow has committed. This chapter has one of each.

rust email_address = "0.2";
// the crate's parser decides whether an address is well formed; runs only in the service
effect well_formed(addr: string(64)) -> bool
    impl { email_address::EmailAddress::is_valid(&addr) }
    fixtures { ("ada@example.com") => true; ("ada at example") => false; }
events { Subscribed(subscriber: id) }
row Subscriber { id: id, addr: string(64) }
unit List {
    caps storage, outbox;
    state subscribers: Subscriber[16];
    contract add(subscriber: id, addr: string(64), well_formed: bool) {
        case !well_formed => fail BadAddress;
        else => Subscribed: subscribers += [Subscriber { id: subscriber, addr }], emit Subscribed(subscriber);
    }
}
flow subscribe(subscriber: id, addr: string(64)) atomic {
    let ok = well_formed(addr);
    List.add(subscriber, addr, ok);
}
deliver Subscribed to webhook env "CRM_HOOK";
deliver Subscribed to mail "list@example.com";
scenario two_addresses {
    subscribe(1, "ada@example.com") => Subscribed;
    subscribe(2, "ada at example") => BadAddress;
}

An effect

effect well_formed(addr: string(64)) -> bool is declared like a function, with a typed header, and has two bodies. impl { … } is the Rust that runs in a service. fixtures { … } are literal answers for literal arguments, used when the program is verified. rust email_address = "0.2"; names the crate the Rust uses, and the generated service’s manifest gets exactly that line.

That is how a Rust crate enters a Vishy program: inside an effect, behind a header the rest of the program can read. The program sees (string(64)) -> bool. It never sees the parser. (The language has one other place for Rust, a function with an impl body, kept as an escape hatch; vishy verify refuses to run one, and this guide never uses it.)

Flows call effects; contracts do not

subscribe calls the effect, binds its answer with let, and passes it to List.add as an ordinary argument. The contract decides what an unusable address means, fail BadAddress; the effect only reports a fact. A contract that asks the effect itself is refused:

effect well_formed(addr: string(64)) -> bool
    impl { addr.contains('@') }
    fixtures { ("ada@example.com") => true; }
row Subscriber { id: id, addr: string(64) }
unit List {
    state subscribers: Subscriber[16];
    contract add(subscriber: id, addr: string(64)) {
        case !well_formed(addr) => fail BadAddress;
        else => Subscribed: subscribers += [Subscriber { id: subscriber, addr }];
    }
}

book/refusals/effects-in-contract.vish:8:15: error: unknown function `well_formed`
          case !well_formed(addr) => fail BadAddress;
                ^^^^^^^^^^^

Inside a contract the effect’s name does not exist. A contract reads its unit’s state and its arguments and nothing else, which is what lets the verifier call it from any state it likes. The first removal holds here too: nothing outside the unit can reach in, and a contract cannot reach out.

In verification the effect never runs

scenario two_addresses
  subscribe(1, "ada@example.com") => Subscribed
  subscribe(2, "ada at example") => BadAddress
  List = List { subscribers: [Subscriber { id: 1, addr: "ada@example.com" }], outbox: [Subscribed { subscriber: 1 }] }
2 step(s), all as expected

verify: 0 examples, 2 scenario steps and 2000 sampled checks passed

The scenario’s two calls got their answers from the fixtures. In the sampled checks, where no fixture matches the argument, the verifier samples the effect’s answer by its type, so List.add is checked with both true and false for any address. The Rust is never compiled or called. To see how little the verdict depends on it, replace the impl body with panic!("the address checker is down"): on 30 Sept 2026 vishy verify still answered verify: 0 examples, 2 scenario steps and 2000 sampled checks passed.

What the verifier trusts is the header and the fixtures. An effect that can answer anything its type allows has to be met by a contract that handles anything its type allows.

In the service the Rust runs

Built with vishy service and cargo build --release, the same program ran its Rust. On the service’s command line, 30 Sept 2026:

$ service e.db acme subscribe 1 ada@example.com
Subscribed
event Subscribed { subscriber: 1 }
$ service e.db acme subscribe 3 'ada@@example.com'
BadAddress

No fixture mentions ada@@example.com; the crate’s parser refused it, and the contract turned that into the program’s own failure (exit status 4 on the command line, 409 at a door). The version whose Rust panics, given a route and served, answered each request with 500 {"error":"internal: the address checker is down","flow":"subscribe"}, served the next request, and afterwards dump showed no subscriber and outbox no event: a panic inside a flow writes nothing.

Deliveries

emit Subscribed(subscriber) puts an event in the unit’s outbox; caps outbox allows it. Where the event then goes is one line per destination:

deliver Event to webhook "https://…"; posts it to a URL,
deliver Event to webhook env "NAME"; reads the URL from an environment variable when it delivers,
deliver Event to mail "ops@example.com"; posts {to, subject, event} to the endpoint in VISHY_MAIL_HOOK,
deliver Event to effect name; calls a declared effect (body: string(n)) -> bool with the event as JSON.

The program declares the destinations; the service does the delivering. When the flow commits, the service writes one outbox row per event and destination in the same transaction as the state change, so an event is never lost and never recorded without its cause. A drainer, run by serve every 500 ms or by deliver once, posts each row. From the same session:

$ service e.db acme outbox
1 Subscribed -> webhook-env:CRM_HOOK attempts 0 delivered_at - error -
2 Subscribed -> mail:list@example.com attempts 0 delivered_at - error -
$ service e.db acme deliver
… "attempt":1,"ok":false,"error":"no destination for `webhook-env:CRM_HOOK` (set the environment variable)","next_in_ms":1000}
… "attempt":1,"ok":false,"error":"no destination for `mail:list@example.com` (set the environment variable)","next_in_ms":1000}
delivered 0, failed 2 (retried later)
$ CRM_HOOK=http://127.0.0.1:18741/crm VISHY_MAIL_HOOK=http://127.0.0.1:18741/mail service e.db acme deliver
… "attempt":2,"ok":true}
… "attempt":2,"ok":true}
delivered 2, failed 0 (retried later)

The listener received {"event":"Subscribed","subscriber":1} with the header Idempotency-Key: acme-1, the tenant and the row, the same on every retry. A failure waits and tries again, doubling the wait from one second to a few minutes at most, for up to twenty attempts, and then stays listed by outbox for a person to read. Delivery is at least once; the key is how a receiver drops a repeat. An effect destination is delivered when it answers true and retried when it answers false or panics, which makes any crate a destination: a queue client, a broker, a mail library, with the Rust inside the effect and the choice of destination one line of Vishy.

The verifier delivers nothing. What it can check is that the right events were emitted: the run above ends with outbox: [Subscribed { subscriber: 1 }], and a contract can say ensures emitted([…]).

Try

Change the fixture ("ada at example") => false to => true. The scenario’s second step now gets Subscribed, and vishy verify fails naming that step and the world it reached. The fixtures are what the verifier believes about the world, so a wrong fixture is a wrong belief, found where it matters.

Keyboard shortcuts