# 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:

```jadpo
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](/docs/project-layout-and-modules.md)). 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:

```jadpo
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
    }
}
```

```jadpo
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:

| It does | So |
|---|---|
| Works a value out, calls a function, raises any failure | Read-only |
| Reads with `get`, `history` or a query; `sessions.tokens`, `<Service>.keys`, `batches.status` | Read-only |
| Calls a provider's operation that changes nothing: `changes: false`, or a `GET` operation that doesn't say | Read-only |
| Asks a model: `ai.embed`, `ai.embed_all`, `ai.generate`, `ai.stream` ([Generating changes nothing at the provider](/docs/ai.md)) | Read-only |
| A store's `read` | Read-only |
| `create`, `update`, `delete`, a counter, a transition, `erase` or `export` | Not read-only |
| `sessions.start`, `sessions.end`, issuing or revoking a token or a key, a magic link's request or redemption | Not read-only |
| Starting or cancelling a run (`batches.each`, `batches.cancel`, a file helper) | Not read-only: each keeps a row |
| `emit`, of an event or an email, which is how a job starts | Not read-only |
| A provider's operation with `changes: true`, even an idempotent one, or a store's `put` | Not read-only |
| Calls another action, a package's among them | Whatever that action does |

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](/docs/ai.md)), 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](/docs/access-records.md) 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](/docs/service-credentials.md)). 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:

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