What a route runs

run: calls one named action. It passes the placeholders, input and the caller as ordinary arguments. A GET calls a named query instead, or an action that only reads, so it can never write, as HTTP promises of a GET, and a read needs no action wrapped around its query:

GET /{todo_id: Todo.id} {    output: TodoView    run: todo_view(todo_id)}POST /{todo_id: Todo.id}/complete {    output: TodoView    run: complete_todo(todo_id)}

The query todo_view lives in its domain's queries/ folder, and the action complete_todo in actions/. Your own domain's actions and queries are called by their names. Another domain's public ones are called through that domain's name, as in billing.charge(order) (Project layout and modules). A route can't hold an action of its own written inline.

A GET that runs an action

A query says what to read. A GET that has to work a value out, raise more than one failure or ask a model runs an action instead, as long as the compiler can prove the action only reads. It proves that from the graph: the action writes nothing, emits nothing and makes no changing call, itself and through every action it calls.

Here GET /tanks/{tank_id}/left works out whether a tank has room left. It can fail two ways, so it answers 404 for a tank that isn't there and 422 for a reading past the tank's end:

use storage/entities { Tank, TankNotFound }use storage/types { LeftAsked, LeftView }use storage/failures { PastTheEnd }action room_left(tank_id: Tank.id, asked: LeftAsked) fails TankNotFound, PastTheEnd -> LeftView {    var tank: Tank = attempt Tank.get(tank_id)    if (asked.used > tank.notches) {        reject PastTheEnd {}    }    return LeftView {        has_room: asked.used < tank.notches    }}

use storage/entities { Tank }use storage/types { LeftAsked, LeftView }use storage/actions { room_left }routes Tanks {    prefix: /tanks    GET /{tank_id: Tank.id}/left {        authentication: RouteAuthentication.none        input: LeftAsked        output: LeftView        run: room_left(tank_id, input)    }}

What the proof counts:

Anything on any way through the action counts: a write in one branch of an if is has_room. A function needs no looking into, since a function can't do any of these. Anything else makes the route route.run_kind, whose message names what the action does and where, following the calls.

What Jadpo keeps for itself is not the action's doing, and a GET that calls a model or a provider may still cause it: a model's use is counted against ai: { limits: } (Budgets), and a provider's circuit breaker and the rate limits count their own. Each is done in a statement of its own, or in memory, never in the action's transaction. Signing a caller in reads and changes nothing. A GET keeps no Idempotency-Key, so a model or a provider that changes nothing is sent none of the keys derived from one. Reads leave no record: the audit trail only records changes, and the access records aren't built yet; when they are, they go in a statement of their own for a query and an action alike.

The runtime holds what a GET runs to the same line, its query or its action. Its transaction is begun READ ONLY, so PostgreSQL itself refuses a write. Asking to write, to keep an event or to make a changing call answers 500 internal_fault and keeps nothing. The proof means checked code never gets there, so reaching it is a bug in Jadpo.

Everything else about a GET stays as it was. HEAD runs the same action and sends the same head with no body, so a HEAD of a route that calls a model calls the model. Its input is its query string, there is no settle: to set, since nothing was set off, and browsers and caches may repeat it. A GET calling a model costs money each time it's repeated: ai: { limits: } caps that, and a route that should not be open to the world says who may call it, as any route does.

Listing tokens and keys

A GET can also run the listings Jadpo generates for sign-in credentials. sessions.tokens(user_id) lists the tokens a user holds, and <Service>.keys(service_id) the keys a service holds (Service credentials). They read the tokens and keys the runtime keeps, so a route lists them without an action that copies each one into an Output.

The route passes the holder's id, from a placeholder or from current_principal. Its output: is the List<IssuedToken> or List<IssuedKey> the listing returns, exactly as for a named query:

GET /devices {    output: List<IssuedToken>    run: sessions.tokens(current_principal.user.id)}