# What a run reaches under policy

A batch's actions run as the system, but what they do still answers to
the policy of the people who started the run or read its status. This
topic says what Jadpo checks so that a batch never leaks a record to
someone who may not read it.

## What the summary carries

An `ImportSummary` holds counts and problems, never a record's fields.
`items` shows nothing of the items the run walked, as a count of a
query's records doesn't. `items_with_problems` and `problems` count the
items whose action failed, and say which and why. So they carry what
decides whether `each:`'s action fails: what decided each `reject` and
`attempt` it runs, and whether an action it calls fails, read from the
item and from what the run saved. What decided that the run starts goes
with all three.

## The item is checked like any call's argument

Each item is one of the records `from:` finds, and it is the same record
all through `each:`'s action. So what that action stores from it, given
the item or a field of it, is checked where `each:` calls it, as a
call's arguments are.

## A saved value has left its record

What a run saves has left its record, as a value an event carries has
([Subscribers](subscribers.md)): the record may change while the run goes
on. So it is checked as a value that could have come from any record of
its entity. The one exception is a record a saved tenant id was read
from, which is known to be of the tenant the run is limited to. A value
the starting action was passed is checked where that action is called,
in the same way.

## The run's tenant proves what it reaches

Every record a run reads is of the tenant it is limited to. So the item,
and what decided its action's failures, may be stored wherever that
tenant's roles may read them, as a record of an event's tenant may. A
record every tenant shares (`Tenancy.shared`) isn't the tenant's.

## Every action a run reaches is checked

What a schedule, a subscriber or a batch reaches is checked against the
line under `actions:` of every action it reaches, not only the one it
runs ([Actions](actions.md)). A listed action's line decides
its own body's writes wherever it is called from. Routes are checked the
same way.

## What the run's actions show

Nothing reaches whoever started the run. A failure's fields, and a
record found by a value, are shown to nobody, and a problem keeps only
the failure's code.

## What `batches.status` shows

Where `batches.status` is read, nothing says which batch a `BatchRun` is,
since a run is found by its `id` alone. So what it gives is held to what
decides the failures of every batch the app starts: whether each one's
`each:` action fails, and whether its `finished:` action fails, which
ends the run `failed`. Each is checked as though it came from any record
of its entity, never one of a run's tenant, and with nothing of what the
starting action was passed.

The reader is checked only by what the reading action's line under
`actions:` lets in as it starts. A status read inside a batch's own
actions goes round in a circle, and is worked out as calls that go round
are.

So in an app with a tenant, a run's status shows only what anyone at
all, or a role held across the whole app, may read. Letting a reader in
through the record that keeps the run would need the `BatchRun` to say
which batch and tenant it is.

## No request carries a batch type

A request can't name a run. An `Input`, read from a body or, for a `GET`
or a `DELETE`, from the query string, and a route's placeholder may not
hold a `BatchRun`, a `BatchProgress`, a `RowProblem` or an
`ImportSummary`. That holds whether the type is there directly, in a
list, a map or an option, in an object, through a type built on one, or
through an entity's field holding one (`Sweep.run`); each is
`type.batch_input`. A `BatchState` is a plain enum a request may name.

A named query's parameter isn't refused, because what is passed to it
comes from a route's placeholder or input, which are checked, or from an
action. A batch type's fields can be read
([Other built-in types](built-in-types.md#other-built-in-types)),
but one named as a type, such as `BatchRun.id`, is `type.unknown_field`,
as is a field a standard object doesn't have. A run is reached from
`batches.each`, or from a field the caller may read.

Here `each:`'s action stores part of the item where more people can read
it: `post_item` puts a diary's confession, which only its owner may
read, on a board anyone signed in may read. Jadpo follows the item into
the action and refuses the call:

```jadpo
action post_item(diary: Diary) -> Unit {
    var board_post: Board = Board.create {
        set: {
            text: diary.confession
        }
    }
    assert board_post.text == board_post.text
}

action post_all(page: DiaryPage) -> BatchRun {
    return batches.each(from: diaries(page), each: diary -> post_item(diary))
}
```

```text
error: `post_all` passes `Diary.confession` to `post_item`, which stores it in `Board.text`, though not everyone who may read `text` may read it
 --> main.jadpo:11:71
   |
11 |     return batches.each(from: diaries(page), each: diary -> post_item(diary))
   |                                                                       ^^^^^ from `Diary.confession`
  reason: `post_item` stores what it is given here in `Board.text`, and everyone who may read `Board.text`, anyone signed in among them, reads what is stored there, from any request, and only the user `owner_id` points at and schedules and subscribers may read `confession`. A value stored in a field keeps its own field's rules, as one sent in an output does, so it is stored only where everyone who may read it may read the value.
  next: Pass `post_item` what everyone who may read `Board.text` may read, or give `text`'s `read:` only those who may read `confession` (agent)
  rule: policy.output_field_unproved
  help: https://jadpo.dev/docs/errors/policy.output_field_unproved

check failed: 1 error, 2 files
```

Here a run's status leaks what decided its failures. `check_diary` fails
on a diary whose confession says "draft", so the number of problems
tells the reader something about confessions. `count_drafts` shows that
number to anyone signed in, which its line under `actions:` lets in:

```jadpo
type Draft = Failure {
    kind: FailureKind.rejected
    message: "This diary is a draft."
}

type DraftCount = Output {
    drafts: Int
}

action check_diary(diary: Diary) fails Draft -> Unit {
    if (diary.confession == "draft") {
        reject Draft {}
    }
}

action check_all(page: DiaryPage) -> BatchRun {
    return batches.each(from: diaries(page), each: diary -> check_diary(diary))
}

action count_drafts(draft_walk: BatchRun) -> DraftCount {
    var at: BatchProgress = batches.status(draft_walk)
    return DraftCount {
        drafts: at.problems
    }
}
```

```text
error: `DraftCount.drafts` carries `Diary.confession`, which not every caller of `count_drafts` may read
 --> main.jadpo:23:17
   |
23 |         drafts: at.problems
   |                 ^^^^^^^^^^^ decided by `Diary.confession`
  reason: `batches.status` finds a run by its `id` alone, so what it gives shows what decides the failures of every batch the application starts, `Diary.confession` among them, to anyone who may call `count_drafts`, and only the user `owner_id` points at and schedules and subscribers may read `confession`.
  next: Let only those who may read `confession` call `count_drafts`, through its line under `actions:`, or decide which items fail by what its callers may read (agent)
  rule: policy.output_field_unproved
  help: https://jadpo.dev/docs/errors/policy.output_field_unproved

check failed: 1 error, 2 files
```

A route can't take a run in its path:

```jadpo
routes Sweeps {
    prefix: /sweeps

    DELETE /{shelf_run: BatchRun} {
        authentication: RouteAuthentication.none
        status: SuccessStatus.no_content
        run: stop_sweep(shelf_run)
    }
}
```

```text
error: Placeholder `shelf_run` holds a `BatchRun`, which no request carries
 --> main.jadpo:4:25
  |
4 |     DELETE /{shelf_run: BatchRun} {
  |                         ^^^^^^^^ a `BatchRun`
  reason: Only the runtime builds a `BatchRun`: a run comes from `batches.each`, or from a field the caller may read where the application kept it, and `batches.status` and `batches.cancel` find it by its `id` alone. A request that named one could read or stop any run.
  next: Take the `id` of the record that keeps the run, and read the `BatchRun` from its field (agent)
  rule: type.batch_input
  help: https://jadpo.dev/docs/errors/type.batch_input

check failed: 1 error, 2 files
```