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): 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). 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), 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:

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))}

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

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

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_unprovedcheck failed: 1 error, 2 files

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

routes Sweeps {    prefix: /sweeps    DELETE /{shelf_run: BatchRun} {        authentication: RouteAuthentication.none        status: SuccessStatus.no_content        run: stop_sweep(shelf_run)    }}

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_inputcheck failed: 1 error, 2 files