Enum Effect 

pub enum Effect {
    Read,
    Write {
        domain: Address,
    },
    Egress,
    Connector {
        label: ServerLabel,
    },
    Spawn,
    Govern,
    AttachUserBrowser {
        address: Option<String>,
    },
    Spend,
}

What kind of boundary a call crosses — this field routes the call to its gate; it is machine input, not documentation.

Variants

Read

Write

Fields

domain: Address

Egress

Leaves this machine for a destination the call names.

Connector

Leaves this process for an external server the building configured. The destination is fixed by the registration rather than named per call, because every call to one connector tool goes to the same place — and a model filling in a host argument would be inventing a fact the city already knows.

Fields

label: ServerLabel

Spawn

Starts a second agent on part of this work. Its own class rather than a Read: what a spawn costs and what it can reach is not bounded by anything the calling run’s other gates check, and the only thing that bounds it is the person.

Govern

Changes what governs a scope - the rules its own runs are judged by. Deliberately not a Write: the reserved subtree is outside every write domain, so the write door would refuse it, and the reason it refuses is that this decision is the person’s.

AttachUserBrowser

Attaches to a browser the person is already driving, with that person’s own login state.

Its own class rather than an Egress: the bytes a call sends are the smaller half of what it reaches for, and a run allowed to open pages in a browser this city started has not thereby been granted every account that browser is signed into. The address is the registration’s, not the call’s; None is a person who enabled the tool without saying where it answers, which the attach door answers with a question.

Fields

address: Option<String>

Spend

Moves money. No tool in this build declares it; the bench refuses it with E_TOOL_UNAVAILABLE, so the first tool that does meets a door rather than a gap (crates/runtime/spec/Tools.lean).

Trait Implementations

impl Clone for Effect

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Effect

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Effect

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for Effect

impl PartialEq for Effect

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for Effect

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Effect