membrane, Permissions as Casts

Most systems bolt permissions on as an afterthought: an ACL consulted at the door. Osmol types them. A membrane rule is a granularity cast, a typed statement of how much precision a given audience may receive, and the whole family of upward casts simply does not exist in the grammar. Privacy in Osmol is not a filter that fights at runtime; it is a property of which sentences can be written.

Syntax

From the grammar in spec §5:

membrane    = "membrane" "{" { flowrule } "}" ;
flowrule    = selector "->" party [ "when" condition ] ":" transform ;

selector    = fact | ident | "*" ;
party       = ident | "@role(" rolename ")"
            | "family" | "team" | "others" | "all" ;
transform   = "exact" | "coarse(" grain ")" | "category"
            | "existence" | "deny" ;

Each rule reads: facts matching this selector, flowing to this party, (optionally) when this condition holds, cross at this grain.

Semantics

The six-rule example from spec §4.7:

membrane {
  eta(*)        -> family:                exact
  eta(*)        -> others:                coarse(30m)
  location(*)   -> family when moving:    exact
  location(*)   -> others:                coarse(city)
  status(atlas.*) -> @role(lead, atlas):  exact
  finances(*)   -> all:                   deny
}

Transforms are downward casts. The five transforms are the four rungs of the granularity lattice (exact, coarse(g), category, existence) plus deny, which is the zero of the whole system. There is no syntax for an upward cast: you cannot write a rule that turns coarse(city) into exact, because the grammar's transform vocabulary has no word for refinement. Axiom IV, precision only flows downhill, is enforced by the parser's dictionary before any checker runs. Where a program tries to grant a grain finer than the holding actually has, the semantic checker answers with O-002.

Membranes belong to the twin they are inside. A membrane block governs the outbound flow of its own twin's holdings, and nothing else. The grammar cannot express "raj's membrane" from inside maya's twin; attempting to reference another twin's membrane or attention is O-006, and Axiom III is the reason: the receiver's grammar governs, and the sender's membrane governs the sender.

Selectors are fact patterns with * wildcards and dotted paths. eta(*) matches any eta fact; status(atlas.*) matches status(atlas.review) and everything else under the atlas project; a bare * matches all facts. Specific and general rules coexist; order decides between them (below).

Parties name the audience: a specific twin by name (raj), a semantic role (@role(lead, atlas)) resolved at flow time rather than bound to an endpoint, or one of the four audience classes family, team, others, all.

Conditions (when moving) gate a rule on the twin's own state, so precision can depend on context: exact location for family, but only while in transit.

The audit trail (future). The Osmosis protocol spec (§4) requires that every membrane decision be logged in an append-only record visible to the membrane's owner, and that the membrane be portable: its policy set and logs export in a standard format and rehost on any conforming mesh without loss. That portability is one of the two constitutional clauses of Osmol governance. No wire transport exists yet, so no implementation writes this log today, but any future one must.

Cast weights

Inside the pressure function P = R × U × T × M − C, the membrane's verdict becomes the factor M:

deny annihilates pressure entirely, and this is exactly the shape Theorem 2 (non-interference) needs, once it is proven: M = 0 means no delta derived from this twin's state can reach that party at all.

In the v0.1 interpreter

osmol.py implements membranes in membrane_cast, with four documented behaviors to honor or consciously supersede (see v0.1 pragmas):

• Rules match in declaration order, and the first match wins. Put specific rules above general ones; a leading eta(*) -> all: deny shadows everything after it for eta facts.
• No matching rule means no flow. membrane_cast returns None, and the engine treats that exactly like deny: default-deny is the resting state of every membrane. A twin with an empty membrane block shares nothing.
• The circles pragma. v0.1 has no social graph, so audience classes are derived from bonds: family and team match any party the sender bonds trust high; others matches everyone else; all matches everyone. This is why the dinner mesh's maya must bond raj { trust high } for her eta(*) -> family: exact rule to reach him.
• when conditions are parsed but not evaluated. The condition is captured into the rule tuple and then ignored: a when moving clause in v0.1 behaves as if always true. This is an honest gap between grammar and engine, and a good first RFC-shaped contribution.

Related

• The granularity lattice, what the casts are casts on.
• O-002, granularity inversion: precision cannot be manufactured, only surrendered.
• O-004, no membrane rule may match an express; the human lane is verbatim.
• O-006, foreign sovereignty: membranes and thresholds belong to their owners.