Yichus/Access
Builtin package (resource access.bosatsu).
This is the complete package source used by this build. The export
list names its public API; definitions below give the types and behavior.
New to the API? Start with Make a calculator or Build an API, then use this page to look up a definition.
package Yichus/Access
# Canonical data-access rules for Yichus APIs. Author-facing
# policy modeling lives here; Yichus owns the analysis and the runtime
# that constructs `Principal` at the trust boundary.
#
# Verified statically by the access analyzer (`AccessAnalyzer` on the
# JVM and in the API-safety MCP bundle); a `Withheld` declaration is
# checked by `api verify`'s `stored-field-disclosure` property.
#
# The model is deliberately small so every claim is provable from the
# typed Matchless IR:
#
# - `Principal` is the authenticated caller. It is constructed by the
# runtime at the trust boundary, never by handler code.
# - A resource with `OwnerScoped` policy stores rows keyed by exactly
# `Principal.user_id`, or multiple rows per user keyed by
# `owner_key(principal, local_key)`. The analyzer proves that
# every `db_read` / `db_write` / `db_delete` key on that table is
# derived from the authenticated caller by one of those two forms,
# and that no unkeyed operation (`db_create`,
# `db_query`) touches the table.
# - A resource with `Public` policy is readable and writable by any
# caller; no key discipline is required or claimed.
# - `PublicReadRoleWrite(roles)` permits reads and queries on any route,
# including anonymous routes. Every create, update, delete, or ID allocation
# must be reachable only through routes requiring every declared role.
# - A resource with `GuardedOrRoles(guards, roles)` follows the same row
# guard rules as `Guarded` on ordinary routes. A binding may instead use
# the resource without a row guard only when it is reachable from at least
# one declared route and every route that reaches it requires every role
# in `roles`. Route and call reachability come from typed IR; an unrouted,
# mixed-authority, or unresolved helper receives no role proof.
# An empty guards list makes the resource role-only: every operation,
# including creation, requires this route authority.
# - A resource with `Guarded(guards)` policy holds rows whose visibility
# and mutability are decided by declared predicates ("guards"): pure
# `Bool`-returning bindings in the spec's package, named in `guards`,
# that take the caller's `user_id` and a row. The analyzer proves,
# by branch dominance over the typed IR, that
# * every `db_write` / `db_delete` on the table is either a create
# (keyed by a `db_next_id` of the same table) or sits inside the
# true branch of a guard applied to `Principal.user_id` and a
# row read from a Guarded table;
# * every value derived from a row read from the table (the row, a
# field of it, anything computed from it) is used only inside
# such a branch, as an argument to a guard, as a match
# scrutinee, or as the rows of `keep_visible` filtered by a
# guard — until a guard branch has vouched for it, after which
# it may reach the response.
# The finding at each site names the guards that dominate it; the
# reader judges whether they are the right ones. Nothing about the
# guard's body is checked beyond its type: the guard IS the rule.
#
# Declare the rules as an `AccessSpec` binding. Discovery is structural
# (any binding whose checked type is `AccessSpec` participates), so the
# spec survives renames, moves, and other agent edits to the file.
from Bosatsu/Predef import List, concat_String, int_to_String, length_String
export (
Principal(),
Policy(),
AccessRule(),
AccessSpec(),
Release(),
Withheld(),
owner_key,
keep_visible,
reveal,
)
# The authenticated caller: a stable user id plus role names.
# `roles` is RESERVED: access decisions must not branch on it. Role-protected
# server entry points declare `RequiresRoles` in `Yichus/Service`; the runtime
# checks those roles before handler invocation and does not expose the verified
# claim through this field. It remains here for Principal shape compatibility.
# Handlers that touch owner-scoped data must take a Principal and
# derive their DB keys from `user_id`.
struct Principal(user_id: String, roles: List[String])
# A collision-free key for one of several rows owned by the authenticated
# caller. The decimal length prefix makes (user_id, local_key) injective even
# when either string contains separators. The access analyzer recognizes this
# exact typed call and requires `principal` to derive from the handler's
# runtime-injected Principal; hand-built or request-supplied values prove
# nothing.
def owner_key(principal: Principal, local_key: String) -> String:
Principal(user_id, _) = principal
concat_String([int_to_String(length_String(user_id)), ":", user_id, local_key])
# Per-resource access policy.
enum Policy:
Public
OwnerScoped
Guarded(guards: List[String])
GuardedOrRoles(guards: List[String], roles: List[String])
PublicReadRoleWrite(roles: List[String])
# Filters rows read from a Guarded table by a guard. The analyzer
# accepts a `db_query` result of a Guarded table only here, and only
# when `visible` is a lambda whose body applies a declared guard to the
# caller's `user_id` and the row; the result is then clean and may
# reach the response.
def keep_visible[a](rows: List[a], visible: a -> Bool) -> List[a]:
[row for row in rows if visible(row)]
# One rule: the table name (as passed to `Yichus/Data::table`) and the
# policy the analyzer must prove for it.
struct AccessRule(resource: String, policy: Policy)
# The complete declared access surface of an API module. Every table a
# handler touches must be covered by exactly one rule; an operation on
# an undeclared table is a finding, never silently allowed.
struct AccessSpec(rules: List[AccessRule])
# A function a withheld field may reach an exposed route's response
# through: what a call of it returns may be disclosed, and nothing else of
# what it was given. Held like `Yichus/Service::Handler` holds its
# function, so one declaration can list functions of different types; the
# analyzer reads which function from the typed Global reference in the
# Matchless IR, never from a name. Nothing about the function's body is
# checked: the release IS the rule. A function that returns its argument,
# or an invertible function of it, discloses the field. A function released
# is released at every call of it in the program, a `Bosatsu/Predef` one
# too, so release a named function of your own.
# The check follows flow, not values: a stored value returned under a
# released guard is still reported as copied, even when it must equal the
# caller's input (the answer returned only when matches(answer, guess)
# holds), so return the caller's own input there instead.
# Releasing an equality test makes it an oracle: a caller can try values
# until one is accepted. The check judges one response and does not count
# calls, so bound the guesses with `limited` or `limited_by` on the route.
struct Release(run: exists a. a)
def reveal[a](run: a) -> Release:
Release(run)
# Fields of `table`'s rows that no exposed route (a `public_route`, or a
# `publishable_route` answering someone an account gave its key to) may
# answer with, except through a call of one of `releases`. Each path names
# a field of the table's checked row type, as the reach report renders
# it: `questions[].answer` is the `answer` of every element of the row's
# `questions` list, an enum's field is preceded by its constructor
# (`Locked.note`), and a leading `[]` steps into a `Table[List[a]]` row.
# Write each declaration as its own top-level binding, literally:
# name = Withheld("table", ["path", ...], [reveal(f), ...])
# with `f` a top-level function definition (`Release(f)` also works).
# Only the named paths are judged: another stored field computed from a
# withheld value (a label or key built from the answer) carries the same
# secret, so name it too.
# Anything else fails the check loudly: a Withheld inside another value
# or behind a `def`; a table, path or list that is not a literal; a table
# the program opens with no one checked row type; a path that names no
# field; no path; a release that is a value or a lambda, or is written
# through a helper; a table declared by two bindings. Discovery is
# structural, as for `AccessSpec`: any binding whose checked type is
# `Withheld` participates.
struct Withheld(table: String, paths: List[String], releases: List[Release])