`PW5048`

control_where_refused

The program must hold to this: a control whose command requires a predicate is shown where the page asks that predicate of its reader and it holds.

A program the compiler refuses with it

Refused: PW5048

module guard

import context.{ current_session }
import capability.{ Session, SessionId }

opaque type InteractionId = String

type Post = Post { id: String, text: String }

type PostError =
    | Unavailable

predicate SignedIn
    says "Sign in to post."

fn publish(s: Session<SessionId>, text: String) -> Result<Post, PostError> !{ database.write<Post> }
    host "blog:data/posts#publish"

command post(text: String) -> Result<Post, PostError>
    requires      SignedIn
    idempotent_by InteractionId
{
    publish(current_session(), text)
}

page Write() {
    route "/write"

    signal sent: Int = 0

    view {
        <title>Write</title>
        <button type="button" on:press={() => match post("Hello") {
            Ok(_) => sent = sent + 1,
            Err(_) => (),
        }}>Post</button>
    }
}

pw check

error: [PW5048] this control sends `post`, which `requires SignedIn`, and is shown where the page does not ask `SignedIn`
  --> guard.pw:33:9
   |
26 | /  page Write() {
27 | |      route "/write"
28 | |
29 | |      signal sent: Int = 0
...  |
33 | |/         <button type="button" on:press={() => match post("Hello") {
34 | ||             Ok(_) => sent = sent + 1,
35 | ||             Err(_) => (),
36 | ||         }}>Post</button>
   | ||________________________^ this control sends `post`, which `requires SignedIn`, and is shown where the page does not ask `SignedIn`
37 | |      }
38 | |  }
   | |__- `Write`
   |
   = note: A press the server refuses was a dead control: the owner, signed out, pressed Post and the post went with no word (2026-10-08). A page asks a predicate of its reader by naming it, and the deployment answers it as it answers `requires`, so a control shown under it is refused only if the reader changed since the page was rendered, and then told where the press was (ADR-0302). `SignedIn` is the program's to declare (`predicate SignedIn says "…"`) where only the deployment knows it.
   = help: show it where `SignedIn` holds: `{#if SignedIn}` around it, or `hidden={!SignedIn}` on it; where no reader's answer can decide it, as in a part served to everyone, mark its event `|refusable`

From A button its reader may not press, in Errors and diagnostics. A test holds the guide's examples to the compiler.

The decisions behind it

0307

Reading the diagnostic

pw check prints the code in brackets, [PW5048], with the sentence above and the place in your program. Errors and diagnostics explains how to read one, and every code is listed with its rule.