Storage and the door
Until now every program lived for one command, and its state was gone when the command ended. This chapter keeps the state between calls and puts a door in front of it: HTTP routes that call flows and answer in JSON.
events { Opened(day: int) }
row Loan { id: id, holder: id, days: int(1, 28) }
unit Desk {
caps storage, outbox;
state day: int = 0;
state open: bool = false;
contract open_day() {
case open => fail AlreadyOpen;
else => Opened: open := true, day += 1, emit Opened(day + 1);
}
}
unit Loans {
caps storage;
state loans: Loan[8];
fixture Three = { loans: [Loan { id: 1, holder: 7, days: 7 }, Loan { id: 2, holder: 7, days: 7 }, Loan { id: 3, holder: 7, days: 7 }] };
contract lend(loan: id, holder: id, days: int(1, 28)) {
case count(l in loans: l.holder == holder) >= 3 => fail TooMany;
else => Lent: loans += [Loan { id: loan, holder, days }];
examples { Three (4, 7, 14) => TooMany; }
}
}
flow open_day() atomic { Desk.open_day(); }
flow lend(loan: id, days: int(1, 28)) uses caller atomic { Loans.lend(loan, caller, days); }
view my_loans() uses caller = where(l in Loans.loans: l.holder == caller);
route POST "/open" => open_day();
route POST "/loans" => lend(loan, days);
route GET "/me/loans" => my_loans();
scenario a_morning {
open_day() => Opened;
open_day() => AlreadyOpen;
as 7 lend(1, 14) => Lent;
as 7 lend(1, 7) => Exists;
as 8 lend(2, 21) => Lent;
as 7 my_loans() => Value([Loan { id: 1, holder: 7, days: 14 }]);
}
A lending shelf: Desk opens and says so with an event, Loans lends at most three loans to each caller, and a view lists the caller’s own. The scenario runs as it always has:
scenario a_morning
open_day() => Opened
open_day() => AlreadyOpen
lend(1, 14) => Lent
lend(1, 7) => Exists
lend(2, 21) => Lent
my_loans() => Value([Loan { id: 1, holder: 7, days: 14 }])
Desk = Desk { day: 1, open: true, outbox: [Opened { day: 1 }] }
Loans = Loans { loans: [Loan { id: 1, holder: 7, days: 14 }, Loan { id: 2, holder: 8, days: 21 }] }
6 step(s), all as expected
verify: 1 examples, 6 scenario steps and 5000 sampled checks passed
What caps storage changes
caps storage; on a unit makes its state persist. Nothing else in the unit changes: its contracts, examples and verdict are the same with or without it. What changes is what the compiler writes for you. vishy schema book/programs/storage-shelf.vish prints the tables, on 30 Sept 2026:
CREATE TABLE IF NOT EXISTS desk_scalars (tenant TEXT NOT NULL PRIMARY KEY, `day` INTEGER NOT NULL DEFAULT 0, `open` INTEGER NOT NULL DEFAULT 0);
CREATE TABLE IF NOT EXISTS loans_loans (tenant TEXT NOT NULL, `id` INTEGER NOT NULL, `holder` INTEGER NOT NULL, `days` INTEGER NOT NULL, PRIMARY KEY (tenant, id));
CREATE TABLE IF NOT EXISTS tokens (tenant TEXT NOT NULL, token TEXT NOT NULL, caller INTEGER NOT NULL, PRIMARY KEY (tenant, token));
One row of scalars per unit, one table per keyed table, and a tokens table because a flow says uses caller. Every row carries a tenant, a string naming whose data it is; a request never sees another tenant’s rows. You write neither the schema nor the code that reads and writes it.
The generated service
vishy service book/programs/storage-shelf.vish out sqlite writes a Rust crate; cargo build --release in out makes one binary, service. Every call to it names a store (a SQLite file, or a Turso URL) and a tenant. Three commands start it:
./target/release/service shelf.db acme migrate
./target/release/service shelf.db acme token 7
./target/release/service shelf.db acme serve 127.0.0.1:8080
migrate creates the tables and answers migrated (store at version 0: tables created where missing); it is safe to run again. token 7 prints a bearer token for caller 7 and keeps it in tokens. serve answers until stopped. Each flow is one transaction: the units it touches are loaded, and written back only when it succeeded. The same binary runs a flow from the command line, service shelf.db acme open_day; docs/deploy.md covers supervisors and backups.
The door’s answers
The check that keeps this guide true builds this service, starts it, and calls the first POST route with an empty JSON body:
POST /open
{"events":[{"day":1,"event":"Opened"}],"ok":true,"outcome":"Opened"}
A success is 200 with ok, the outcome the contract named, and the events the flow emitted, each an object with its name under event. The rest of the door, from one session with the same service on 30 Sept 2026 (a token minted for caller 7):
POST /open {} 409 {"events":[],"ok":false,"outcome":"AlreadyOpen"}
POST /loans {"loan":1,"days":14} no token 401 {"error":"unauthorized: a bearer token is required","flow":"lend"}
POST /loans {"loan":1,"days":30} token 400 {"error":"`days`: expected an integer in 1..28, got 30","flow":"lend"}
POST /loans {"loan":1,"days":14} token 200 {"events":[],"ok":true,"outcome":"Lent"}
POST /loans {"loan":2,"days":7} token 200 {"events":[],"ok":true,"outcome":"Lent"}
GET /me/loans?limit=1&offset=1 token 200 {"offset":1,"ok":true,"total":2,"value":[{"days":7,"holder":7,"id":2}]}
A failed outcome is 409 with the same shape as a success: the program working as written, and nothing stored. A flow that uses caller answers 401 without a token; the caller comes from the token, never from the body. A value outside a bound is 400 naming the parameter and the bound, int(1, 28) written once and enforced here as in the verifier. A GET route to a view reads the stored world with no transaction, and a list comes in pages: limit and offset in the query, total in the answer. Every error body names the flow.
One answer this program cannot give: a panic inside a flow answers 500 with internal: and the message, and writes nothing. A verified contract does not panic; the Rust inside an effect can, and the next chapter shows it.
Bounds are for the verifier
Loan[8] does not mean eight loans; it is how large the verifier lets the table grow in its sampled states. The generated service has no such limit: on its command line, ten loans across four callers were all Lent. A rule that really is about the table’s size says cap(loans), which is the bound while verifying and unbounded in a generated service, so a test size never becomes a production limit.
The development door
Building a service takes a minute. vishy serve <inputs> [addr] --db <file> [--tenant <t>] [--mint <caller>] serves the program straight from source, in the same tables, and --mint 7 prints a token for caller 7 into the file. On this program the six requests above gave the same six answers.
It watches its inputs between requests. Saving the program with >= 2 in place of >= 3 logged {"kind":"reload","ok":true,"ms":19,"version":0}, and the next loan for caller 7 answered TooMany. A save swaps the program in between two requests, so no request is lost; on a thirty-unit program the reload was measured on 30 Sept 2026 at 420 to 513 ms. A save that does not check is logged and the old program keeps serving; so is a change to a stored row without version N;, which the chapter on versions explains.
An input written as a quoted pattern, 'parts/*.vish', is expanded again on every check, so a part saved later is picked up. A program that still has a stub is refused: with one part moved out of the folder, the reload answered the program still has stubs (a part is missing from the door's inputs): Bookings.book, Bookings.cancel, Bookings.clear_room, and moving it back reloaded. A flow that fails after a keep step saves what the kept step wrote: served from a file, a refused attempt answered 409 and was still listed after a restart.
One difference remains between the two doors on 30 Sept 2026: vishy serve still stops a table at its verification bound, answering Full on a ninth loan here, where the generated service lent ten.
Try
Add case len(loans) >= cap(loans) => fail ShelfFull; as the first case of lend. vishy verify still passes: the sampler fills the shelf to eight and reaches the new case. Then read the rule again as the service will: cap(loans) has no bound there, so the case never fires in production, and a real limit is written as a number.