Every observed architectural call must be permitted by its caller’s resolved dependency envelope. An undeclared call is an error, including recursive entry into the same operation and requests satisfied from a query cache.

Read in specification context

An observed operation must not violate a prohibition of any active ancestor, even when its immediate caller permits the call. A violation is an error and retains the prohibition and complete call path.

Read in specification context

A concrete class must implement every inherited abstract method.

Read in specification context

An overriding method must preserve the inherited method’s operation kind and resolved result type.

Read in specification context

A class or context declaration has at most one extends base.

Read in specification context

Contexts are a distinct declaration kind and may inherit only from contexts. An ordinary or abstract class cannot inherit from a context.

Read in specification context

invokes crate::module::Class::method(); permits a call on any instance of the named class or a known subclass. This permission does not require equality with the caller’s receiver.

Read in specification context

creates name: crate::module::Context; declares a fresh owned working context under the given binding name. Its target must resolve to a context declaration. This describes context creation; validation does not perform the allocation.

Read in specification context

Each invocation clause grants a direct dependency. Transitive reachability is derived from those direct edges and does not grant the caller permission to invoke an indirect dependency directly.

Read in specification context

An empty envelope describes a leaf operation with no modeled dependencies. It is distinct from an abstract method, which has no declared envelope.

Read in specification context

Declared calls are permissions: none must occur, and calls may occur in an order different from the order of their envelope clauses.

Read in specification context

reads self.field; permits reading a field declared on this receiver’s class or inherited from a base. Unknown fields and non-self field paths are errors.

Read in specification context

invokes self.method(); permits a call on the current semantic receiver. A matching method on a different receiver does not satisfy that permission.

Read in specification context

A state field is valid only in a context declaration.

Read in specification context

Fields retain their declared identity, input, or state kind, distinguishing identity from changing inputs and local working state.

Read in specification context

Methods retain their declared operation kind: query or fn. Resolving a method’s contract preserves that distinction.

Queries describe memoized semantic products; functions describe ordinary computation. These annotations document boundaries; the model has no evaluator or cache.

Read in specification context

Every method body begins with a triple-quoted description, followed by its envelope or abstract; declaration. The description is retained as prose; method-like text within it adds no dependency permissions.

Read in specification context

forbid transitive crate::module::Class::method; prohibits reaching its target over any permitted nonempty call path. A rejected path identifies the offending method sequence.

Read in specification context

An overriding implementation inherits the prohibitions of the base method.

Prohibitions record design intent even when the permitted graph already excludes the target. Adding a permitted edge must still fail validation if it creates a forbidden path.

Read in specification context

The checker resolves declared calls conservatively, including every known overriding implementation in the supplied model.

Read in specification context

Each named type application must supply exactly the declared number of type arguments. This applies to opaque types, built-in types, parameters, and nested applications; a type parameter takes zero arguments.

Read in specification context

A struct or enum can carry triple-quoted prose immediately inside its opening brace. The parsed declaration retains that text; omitting it is permitted.

Read in specification context

An enum contains named variants in source order. A variant can have no payload, an ordered tuple payload, or named, typed fields. These three shapes remain distinct, including when a tuple or named payload is empty.

Read in specification context

A named field can carry triple-quoted prose immediately before its name. The parsed field retains that text independently of the containing declaration or variant’s prose. At the start of a body, the first prose string describes the container; a description for its first field follows as a second string.

Read in specification context

Structs, enums, and opaque types can declare a nonempty comma-separated list of type parameters in angle brackets. Parameters are available throughout their own declaration and do not become names in other declarations.

Read in specification context

Adjacent named fields, enum variants, and tuple payload elements require a comma separator. A trailing comma before the closing delimiter is optional.

For example:

type Binder<T> {
    """A value under the generic parameters binding its references."""
}

struct Items {
    items: Vec<crate::symbols::Symbol>,
}

enum MethodReceiver {
    Value { mutable_binding: bool },
    Ref {
        """A borrowed receiver with the declared mutability."""
        mutability: Mutability,
    },
}

Read in specification context

An unqualified type name resolves first to a parameter of its declaration, then to a type, class, or context in the same module, then to the built-in prelude. An earlier match shadows a later one.

Read in specification context

An opaque type declares a name and any type parameters without fields or variants. It requires triple-quoted descriptive prose, either inside braces or before a terminating semicolon. A payload inside its body is an error.

Read in specification context

The built-in prelude contains Vec<T>, Option<T>, bool, u32, u64, and String. These names are available without declaring them in the model.

Read in specification context

A type outside the current module requires a crate:: or $cratename:: qualified path. Cross-crate type references require a declared dependency; unqualified lookup does not search other modules or the crate root.

Read in specification context

Semantic value types can refer directly to themselves or to each other, without Box or another storage indirection. Such recursion is not a validation error.

Read in specification context

A struct contains named, typed fields. The parsed declaration retains their names, types, and source order; an empty struct is permitted.

Read in specification context

Parentheses always denote a tuple, including () and a single element with or without a trailing comma. (T) is distinct from T when result types are compared for an override.

Read in specification context

Type expressions are named types with optional generic arguments, or tuples. Generic arguments and tuple elements are themselves type expressions, allowing arbitrary nesting. The parsed expression retains that nesting.

Read in specification context

Named fields have distinct names within a struct or a single enum variant. Different declarations and different variants may reuse field names.

Read in specification context

A value declaration cannot repeat a type parameter’s name.

Read in specification context

Variants have distinct names within an enum. Different enums may reuse a variant name.

Read in specification context

Every type name in a value field, variant payload, class or context field, or method result must resolve. An unknown name is an error even when nested in generic arguments or tuples.

Read in specification context

A variant can carry triple-quoted prose immediately inside its payload’s opening delimiter, or immediately after a unit variant’s name. The parsed variant retains that text independently of other variants.

Read in specification context