Module secure 

§3.5’s security properties, as checks rather than as intentions.

docs/03-type-and-effect-system.md §3.5: “Placement-as-type makes vulnerability classes unrepresentable.” This module is where three of that table’s rows stop being prose:

property	mechanism, here
secrets cannot reach the browser	sendable at every tier crossing, and secret[T] is not
the log holds data, never code or views	storable, checked at compile time
authority is one chokepoint	a cap.* effect is discharged only inside decide’s validator

Two axes, not one

“Is it stored” and “does it cross” are independent questions, and conflating them is how systems end up choosing between an incomplete audit trail and a leak. Beck answers them separately:

	Sendable	Storable
ordinary data	✓	✓	a Str, a model of them
Html	✓	✗	a patch stream crosses; replay recomputes a view rather than reading it back
internal[T]	✗	✓	why an account was suspended: recorded forever, never rendered
secret[T], a closure	✗	✗	a token must reach neither the browser nor the log (§3.7 F5)

The third row was empty until the question “what if you want a table but not a data object” was asked directly. Without it, an event that has to record a fact a client must never see forces a choice between dropping it from the log and trusting that no view renders it.

The others in that table are checked elsewhere and named in the Phase 2 report: ingress/ durable being undischargeable on the client is crate::place; escaping in html"" is crate::html; effect-derived NetworkPolicy and grants are beck-infra; the macro phase’s capability restriction is beck-macro; and the tamper-evident history is the replay harness.

What “crosses a boundary” means concretely

Not every value in a program crosses. In Phase 2’s topology exactly three do, and each is a type the splitter already names:

• the command type — the browser’s entire write surface, client → server;
• the event type — appended to the log, and read back by replay;
• the state type — the fold’s accumulator, which the view consumes and whose rendering the client subscribes to.

So the Sendable check is not a whole-program dataflow analysis; it is three types and the transitive closure of their fields. That is a much stronger position than it sounds: a secret cannot reach the browser without being reachable from one of those three, and if it is, the type says so.

Structs

NotSendable

Why a type may not cross a boundary.

Reach

One step of beck explain flow <T>: where a type is reachable, and whether that is allowed.

Functions

check_boundaries

The per-module half.

check_capabilities

The whole-program half — run once, after linking.

check_security

Run §3.5’s checks over a placed program.

flow

§4.7’s beck explain flow ApiKey: every definition whose signature mentions a type, the tier it runs on, and whether that is a leak.

sendable

May a value of this type cross a tier boundary? §3.5: “Boundary crossings require Sendable; secret[T] isn’t.”

storable

May a value of this type be written to the log?