Dependent Affetto: an owned interaction calculus

Status: revised sibling-language proposal, pass 3. Not adopted, implemented, or mechanically proved.

This document consolidates the discussion following 032, including subsequent dependent typing, compile-time effects, callable modes, named contexts, destruction, cancellation, and final shallow-handler syntax. It deliberately makes design decisions where the conversation left alternatives. This is a new language in the Affetto family, not a compatibility revision: the user's explicit preferences take priority over inherited implementation restrictions. The current language contract remains authoritative only for the independently implementing compiler until explicit adoption. This document does not replace that contract, the implementation goal, or acceptance evidence.

The accompanying outline records pass 1. The plain-text expanded draft preserves pass 2 exactly, including its original relative link spellings. The revision record records pass 3 and its evidence. All examples here describe this proposal; none is a claim of parser or execution support. Mathematical code blocks describe the core, not additional surface syntax.

1. Purpose and limits of the specification

Affetto is an imperative, affine, dependently typed language with an effectful compile-time environment and shallow algebraic control. Its organizing principle is:

Data describes completed interactions. A computation owns an interaction in progress. A callable constructs executions. A handler interprets interactions. Abandonment transfers ownership into retirement.

The public core forms in this document define the language, rather than an exhaustive list of standard-library algorithms. A declaration describes a sum of products. A struct is its single completed alternative. An effect supplies response-indexed alternatives. A function supplies an implementation for an invocation. Modules and handlers package implementations and values. These correspondences share compiler machinery without identifying a type with its inhabitants or an interface with authority to implement it.

This is a closed semantic proposal: its core forms, intrinsic families, reflection descriptors, effects, and failure rules are enumerated below. A construct not generated by those forms is rejected, rather than assigned an implementation-dependent meaning. Standard-library algorithms are ordinary programs over these contracts. Native provider correctness, compiler correctness, resource availability, scheduling fairness, and eventual host response are assumptions or verification obligations, not theorems established by this document.

The core is fully dependent over stable values, not an unrestricted calculus in which types execute arbitrary runtime effects or read changing memory. It supports dependent functions, dependent pairs, indexed data, equality elimination, and runtime indices where representation permits. It does not promise automatic theorem proving, termination of arbitrary programs, or a complete decision procedure for program equivalence.

2. Non-negotiable decisions

1. Values and computations have distinct judgments but one source expression language.
2. Arrow and brace bodies are synonymous: -> expression through the statement boundary means { expression } in every body position.
3. No vertical bars or angle-bracket request patterns are used in source matching.
4. fun Op(args) matches an automatically answered operation. ctl Op(args) @ k exposes its affine reply. A regular pattern matches a completed value in an observed position.
5. Calling k(response) only rearms the original computation. It does not execute it or reinstall the selected handler. There is no primitive source resume keyword.
6. match selects once. handle supplies an observation loop. Explicit loops and queues can manage replies themselves.
7. A computation represents one execution. Repeating effects requires an explicit callable, not repeated forcing of the same owner.
8. Adjusted argument ports prepare left to right to completion or a selected request. Product observation prepares all marked inputs before arm selection.
9. Ownership moves after pattern selection. Guard failure does not replay effects or transfer payloads.
10. Type construction may perform compiler-stage effects. Type comparison never replays those effects.
11. Nominal identity is authentic origin plus static instantiation, never a spelling or unvalidated descriptor hash.
12. General recursion and unbounded loops introduce Tick. Interpreting Tick as unconditional continuation exposes Diverge; Diverge is not a request constructor.
13. Compiler work budgets are independent of Tick and cannot be replenished by nested calls or caught failures.
14. Destruction is observable computation. Cancellation request, stopped application execution, and completed retirement are different events.
15. No safe operation creates source-level undefined behavior. Trusted native providers remain part of the trusted computing base unless actually isolated.

3. Surface grammar and body equivalence

Identifiers use ASCII letters, digits and underscore; the first character is not a digit. Names do not implicitly introduce generic variables. Newline and semicolon separate statements; newlines inside parentheses/brackets or after a comma/operator continue the expression. Strings are UTF-8, with escapes \\, \", \n, \r, \t, \0 and \u{scalar}; invalid Unicode scalars reject. Comments are // to newline and non-nesting /* ... */; /// and //! carry inert documentation. Integer literals are decimal, 0x hexadecimal or 0b binary with internal underscores; malformed or out-of-range literals reject. Decimal floating literals use the expected precision directly. From tightest to loosest, precedence is projection/call/index/postfix !/?, unary operators, multiplication/division/remainder, addition/subtraction, shifts, bitwise and/xor/or, ordering, equality, logical and, logical or. Comparisons do not chain. Checked failures are Abort effects as specified in section 26. CamelCase for types/alternatives and snake_case for values are formatting conventions, not name-resolution rules.

A body is either { statements; final_expression } or -> expression ending at the next uncontinued statement boundary. Empty bodies produce Unit. Separators do not discard the last expression. A body delimiter never determines whether execution is immediate or suspended. Expected contracts determine that.

fun twice(x: Nat): Nat ~ Abort -> x + x

fun twice_again(x: Nat): Nat ~ Abort {
  x + x
}

match number {
  0 -> "zero"
  n { format(n) }
}

A function definition uses : ResultType for its optional result annotation. Thus fun() -> 1 always has an arrow body, not a result annotation. A typed form is fun(): Nat -> 1. This distinction is necessary because type expressions are ordinary expressions. It prevents the parser from guessing whether an expression is a type. Callable types still use their function arrow, as in Fn(own T) -> T. Parenthesize a callable-valued result annotation. GADT constructor results and operation response contracts also use : ResultType, never -> ResultType. An arrow following a declaration header introduces its body. A supplied implementation uses the normal fun-definition grammar.

A function declaration header can continue across a newline before its requirement row or body. A bodyless fun declaration is an operation prototype only inside a type or effect declaration. Declarations are private by default. pub exports a declaration; opaque exports its contract without its representation. Constructor paths resolve authenticated alternatives, including alternatives of an indexed family.

Local bindings are name = expression or mut name = expression. set place = value replaces initialized storage or initializes a moved-out local. own marks transfer where an explicit spelling is useful; owning parameter contracts also request transfer. Parameters are read by default; mut is exclusive access and own is transfer. return, break, and continue leave their respective lexical scopes and trigger cleanup.

Ordinary if is a core conditional with one selected branch. A user-defined cond has ordinary call semantics. To avoid executing both alternatives, pass callables:

cond(flag, then = fun() -> 1, otherwise = fun() -> 0)

Bare with f(arguments) passes the rest of its lexical block as the final computation argument, without adding a binding:

with tick_limit(1000)
with logging(sink)
work()

expands to tick_limit(1000, { logging(sink, { work() }) }). There is no use, no with name = ..., and no trailing then/else or each grammar in this proposal. Parenthesized named arguments suffice. The keyword else cannot be an argument name; the ordinary cond function uses otherwise.

Arguments evaluate in written order. Positional arguments precede named arguments; named arguments may occur in any order, but each formal is supplied once. The mapping from names to formals is resolved before execution. Values are evaluated in source order and installed into their formal slots. Omitted implicit arguments are resolved before execution; acquiring an implicit value may not reorder source effects. Duplicate, unknown, or missing explicit arguments reject.

4. Declarations, data, interfaces, and implementations

A declaration descriptor contains a finite ordered family of alternatives. Each alternative contains an ordered input telescope, a result-index refinement, visibility, and optionally a response telescope/result and implementation code. Input telescopes may contain type-valued or erased members, passing modes, and static constraints.

type Point {
  Point(x: F64, y: F64)
}

type Transfer {
  End
  Failed(error: Error)
  fun Item(own bytes: Bytes): ()
}

effect Console {
  Read(): String
  Write(message: String): ()
}

struct Point(x: F64, y: F64) restricts the descriptor to one completed alternative. enum restricts all alternatives to completed data. effect restricts them to response-bearing alternatives without attached implementations. fun introduces an invocation member, with an optional implementation body inside a declaration. General type permits their union. Each is syntax over the same checked declaration construction operation.

In a mixed type declaration, fun marks a response-bearing alternative. An unmarked alternative constructs completed data. Within an effect declaration, every alternative is response-bearing, so fun can be omitted. Both kinds use a colon for their result annotation. The member kind determines whether that annotation refines the constructed family or specifies an operation response. The parser never guesses from the result expression.

A response-bearing alternative is an open call, not an ordinary completed value. No response, Unit response, and Never response differ:

type Messages {
  End
  fun Yield(): ()
  fun Fail(error: Error): Never
}

End has no continuation. Yield requires acknowledgment. Fail cannot be normally answered, but its reply owns a remainder that must retire if abandoned.

A complete descriptor D has deterministic projections Values(D), Operations(D), Requests(D, R) and Impl(D). Values contains completed alternatives. Requests is a response-indexed GADT. An implementation provides every public responding alternative promised by its interface; it is not a choice of one method. Modules may additionally contain associated types, constants, and other implementations.

type Codec(T: Type) {
  fun Encode(value: T, mut output: Writer): () ~ WriteFailure
  fun Decode(mut input: Reader): Result(T, DecodeError) ~ ReadFailure + Alloc
}

person_codec: Impl(Codec(Person)) = Codec(Person) {
  fun Encode(value, mut output) { encode_person(value, set output) }
  fun Decode(mut input) { decode_person(set input) }
}

type Codec(T: Type) { ... } is ordinary factory sugar: fun Codec(T: Type): Type { descriptor_construction }. There is no stage determined by an argument-list position. Parameterized declarations have one parameter list. Multiple nested applications require explicitly returned callables.

In a value-type position, a declaration descriptor selects Values(D). This type is empty for a pure effect interface. An implementation therefore has type Impl(D). It is not one of D's completed variants. D { fun ... } constructs Impl(D). In an effect position, D selects Operations(D).

Impl(D) is a dependent package with one captured environment and a checked method table. Each static method receives a hidden read, mut, or own receiver. Construction captures the environment once across all methods. It does not construct separate closures that borrow the same environment. Associated type choices become fixed at instance construction. Method projection constructs a callable that borrows or owns the receiver. The public Sigma, record, Callable, and code-building APIs can construct this representation. Impl is a standard factory, not a trusted primitive.

The interface constrains each method's inferred Fn/FnMut/FnOnce mode. A call to an ordinary implementation field calls that method. Calling a responding alternative in an effect position performs a request. Sharing a descriptor schema does not erase this distinction. A control handler packages a driver over computations, not merely a table of response functions.

A responding alternative's optional peg row constrains its attached implementation or its Impl method. Performing the request requires its selected interface slot. It does not execute the implementation's effects before interpretation. An ordinary Impl method call has the method's peg row. A handler driver adds its clause effects to its own outward row. This keeps request requirements separate from provider implementation requirements.

5. Type factories and nominal identity

Types are compile-time values with universe levels. Type-producing functions are ordinary functions:

fun Pair(A: Type, B: Type): Type {
  struct(first: A, second: B)
}

fun identity(T: Type): (Fn(own T) -> T) {
  fun(own value: T): T { value }
}

number = identity(Nat)(42)
pair: Pair(Nat, String) = Pair(Nat, String)(3, "three")

Type-family declarations reserve a family head before checking their alternatives. Explicit family indices are arguments to that head, not unrelated fresh declarations; an alternative may constrain those indices, as in Expr below. Anonymous nominal declaration expressions have compiler-issued lexical sites. Repeating one site with the same normalized static arguments produces the same identity. Another site's identical representation is a different nominal type. Transparent synonyms preserve identity.

type Db = Database
type AppDb = @nominal(Database)
type TxDb = @nominal(Database)

For data, @nominal creates a wrapper around Values(D), with construction visibility controlled by its defining scope. For operations, it creates new routing identities with the original payload and response contracts. It does not recursively rename types mentioned inside those contracts. An adapter must explicitly wrap, unwrap, or rename requests. @nominal does not expose an opaque source representation.

@nominal uses its declaration site and static arguments; it does not use a global allocation counter. It creates a distinct nominal wrapper/protocol identity. Conversion through its defining wrapper is allowed only according to exported constructors. It cannot forge an existing brand. An incompatible definition for the same identity is a compile error, not a cache miss.

Builtin Array has an authentic constructor identity. Array(T,n) agrees with another application of that constructor to equal arguments, not with a user declaration named Array. Source names resolve lexically; intrinsic handles do not.

Nominal origin records are scoped compiler handles. They are not numbers supplied by a library. Serialization records authenticated provenance and is revalidated on load; an address or digest is never alone sufficient authority.

6. Dependent types, universes, and equality

The pure dependent core has variables, predicative universes, dependent functions, dependent pairs, algebraic families, identity types, and their eliminators. Type abbreviates universe U0. Type(i) denotes Ui and Ui : U(i+1). Universe levels are statically solved natural expressions; there is no Type : Type axiom.

A stable index is an immutable value whose use in types does not read live mutable state or require runtime resource ownership. Scalars, immutable structural index data, total pure index functions, compiler type handles, static brands, and erased constructor equality witnesses qualify. A live File owner or mutable place is not an index. It may have an associated stable brand. A reference to a resource in a type never keeps that resource alive by accident.

The core supports:

Pi(x:A).B(x)       dependent function
Sigma(x:A).B(x)    dependent pair
Eq(A,x,y)         identity/equality witness

At runtime, callable dependency is represented by a dependent input telescope and computation result. Type-level functions use total pure reduction. Runtime general recursion belongs to computations and is not an inhabitant-producing proof principle.

struct SizedBytes(n: Nat, own bytes: Buffer(Byte, n))

effect Input {
  Read(n: Nat): Buffer(Byte, n)
}

For Read's request payload p, its response type is Buffer(Byte,p.n). It need not be a single constant type shared by every request. A reply preserves p's stable indices even if the owned payload is transferred out.

GADT constructors state result-index refinements. The descriptor schema writes them as result = Family(arguments); source constructors may append : Family(arguments). The annotation is not an arrow body and does not make the constructor response-bearing:

type Expr(T: Type) {
  Natural(value: Nat): Expr(Nat)
  Boolean(value: Bool): Expr(Bool)
}

Matching Natural refines T to Nat in that arm. Inconsistent constructor equations make an arm unreachable only if the checker can establish the contradiction by constructor disjointness or conversion. Unknown equations require evidence; they are not guessed false.

Definitional equality is alpha/beta equality plus transparent total definitions, primitive reduction on known operands, and structural normalization of data/type applications. It has no extensional function equality, user rewrite plugins, or arbitrary arithmetic solver. Identical neutral terms are equal; distinct neutral f(n) and g(n) are not equated. Eta equality is not required in this core. Evaluation is bounded by compiler policy; exhaustion is an elaboration failure, never a successful inequality judgment.

@equal(A,x,y) over an admitted stable equality domain returns Some(sealed Eq(A,x,y)) on equality and None otherwise. Type equality through this operation is CT-only; stable runtime indices use their admitted total comparison. @transport(family,evidence,value) consumes the value and returns it at the equal indexed type without cloning or changing representation. Such evidence can be supplied explicitly, but no arbitrary Boolean can be cast to Eq. General proof automation is outside this proposal; GADT refinement and safe checked construction do not require it.

Runtime dependent pairs package indices that leave their original lexical scope. Existentially hiding a region does not erase its outlives constraints. Erased indices may be absent from physical storage only when no runtime operation requires their values; otherwise a witness is stored or passed separately.

7. Representation and ordinary array construction

Array(T,n) is inline and requires a statically known, finite target layout. Buffer(T,n) is an owned allocation with a fixed-size handle and may have a runtime n. Slice(r,T,n) is a scoped loan with length n. These are distinct representation contracts, not different levels of dependent typing.

A loop need not come with a user-written induction proof to construct one of these values. Builders track initialization and validate completion:

fun make_four(): Array(Nat, 4) ~ Abort {
  mut builder = ArrayBuilder(Nat, 4).new()
  for i in range(0, 4) {
    set builder.initialize(i, i)
  }
  builder.finish()
}

initialize validates the index and absence of an existing initialized owner. finish validates completeness before publishing Array. Failing completion raises Abort.Uninitialized; the builder still owns and retires all initialized elements. A sequential builder tracks only an initialized prefix; an indexed builder uses initialized-field metadata. Bounds checks may be optimized away when proved, but are not omitted by convention.

A runtime buffer uses explicit allocation authority:

fun make_bytes(n: Nat, heap: Heap): Buffer(Byte, n) ~ Alloc + Abort {
  mut builder = BufferBuilder(Byte, n).allocate(heap)
  for i in range(0, n) {
    set builder.push(0)
  }
  builder.finish()
}

Allocation errors can be returned as Result or converted to Abort by a library wrapper. Alloc alone does not force a particular error policy. Extents are checked against the selected target's positive pointer-offset range; overflow is distinct from exhausted capacity.

Reads through ordinary indexing check bounds and raise Abort.Bounds on failure. A checked Fin(n) constructor permits subsequent unchecked-in-the-core projection because it carries authenticated bounds evidence. It does not confer lifetime or exclusive-access permission.

8. Stages, compiler effects, and persistence

There are two execution stages, CT and RT, using the same core evaluator semantics and different supplied environments. Type, Syntax, Code, compiler Scope, reflection grants and unresolved declaration handles are CT-only. Their validated products can designate runtime code/types without becoming runtime compiler pointers.

A type position demands CT evaluation to a valid type value. An explicit comptime expression or comptime name = expression demands CT execution outside type position. There is no implicit hoisting of effectful RT code merely because its arguments are constants.

comptime codec = derive_codec(Person)
value: derive_record_type(schema) = construct_value()

Mutable CT state may contribute a snapshot:

comptime {
  mut count = 3
  set count += 1
  Four = Array(Byte, count)
  set count = 8
  // Four still denotes Array(Byte, 4).
}

Effectful CT evaluation finishes before its result is inserted into conversion. Equality comparison does not repeat its reads, allocations, diagnostics or nominal creation. An open dependent type expression uses only the pure index language. An effectful factory needs its required inputs before evaluation. The checker does not treat an unknown result as a theorem.

Persistence accepts closed immutable constants, validated descriptors, and checked code whose runtime captures are explicitly represented. It rejects compiler resources, mutable CT storage addresses, reflection grants and live CT loans. Persistent callables do not capture compiler handlers. Generated code executes under its own runtime requirements.

Default CT providers offer bounded allocation, semantic reflection, code construction, diagnostics, target information and declared immutable inputs. The CT root also supplies an always-continue Tick policy inside the independently bounded evaluator. Diverge is permitted within that boundary. This does not change a function's checked row or add a runtime default Tick provider. No automatic environment, clock, random, subprocess, network, host filesystem or FFI provider exists. Imports cannot grant themselves more authority. External preparation is a separate user-authorized process.

9. Implicit parameters, services, and ports

A parameter has name, type, stage, access mode, and explicit/implicit passing mode. A requirement row can combine a named telescope and ordinary interface requirements with +. Generic parameters are ordinary CT parameters. An implicit requirement is satisfied by a named lexical binding or explicit override, never global instance search.

fun encode(value: T, mut output: Writer): ()
  ~ (comptime T: Type, codec: Impl(Codec(T))) + WriteFailure {
  codec.Encode(value, set output)
}

The implicit telescope scopes over the whole signature and is checked in dependency order. A cycle of parameter types without an explicit recursive type declaration rejects. No free name invents an implicit parameter.

Named effects are service slots:

fun transfer(): () ~ (app_db: Database, tx_db: Database) {
  rows = app_db.query(query)
  tx_db.insert(rows)
}

The requirement resolver distinguishes ordinary implicit values from responding interfaces and behavioral markers. An interface slot elaborates to handler evidence for a fresh lexical slot identity. Alpha-renaming a bound slot renames its occurrences, not the nominal Database interface. Two named slots do not collapse merely because their interface types match.

An unlabelled ~ Console + Alloc uses canonical default slot names for those nominal interfaces. Duplicate unlabelled interfaces are idempotent; distinct instances require names or distinct nominal wrappers. Core rows are finite maps from slot identities to interfaces, plus behavioral markers and an optional row tail with lacks constraints. Public signatures are closed unless they explicitly bind a tail. A public function must declare its row, including ~ () for an empty row. A private definition may omit its row and infer it from its body. An explicitly written row constrains private code too. A callable type without a row denotes an empty row; it does not create an unknown effect variable.

Call signatures preserve ports and pegs. A port specifies value/computation input, passing mode, dependency telescope, and selected operation adjustment. The peg specifies produced value, outward requirements, capture constraints and invocation mode. A flat union of all requests is not an adequate replacement.

A ~ E in a value/parameter position means an owned computation port. The same notation in a function result annotation describes that invocation's active result/effect contract. To return a suspended computation rather than execute it, write Susp(A,E,K) explicitly in the result position. E bounds execution requirements; K bounds retirement requirements. Susp(A,E) abbreviates Susp(A,E,E). The short port annotation A ~ E uses the same conservative retirement bound. A more precise port is Port(A,H,E,K), with selected operations H. Plain Susp parameters are value parameters; Port and the ~ parameter syntax request entry preparation. Parenthesization alone does not change this rule. Susp is the ordinary public alias of the core U type; no new evaluation primitive is introduced. A computation-port qualifier also records a preferred observation selection H. Moving the value preserves this qualifier. A raw Susp(A,E) defaults to all requestable, interceptible slots of E; a port annotation can choose H with an explicit residual row. Protected task slots are never part of the default selection.

10. Open and bound computation values

An open computation captures explicitly referenced lexical values but leaves its service slots unsatisfied until it is driven. Supplying a computation to an adjusted port can therefore install the port's interpretation.

Ordinary implicit object parameters are selected when constructing their call. Service requirements of an open computation remain requirements. Explicitly capturing a service object in a closure captures that authority normally.

bind_services(bindings, job) creates an opaque bound computation that owns or borrows the supplied providers. Its exposed requirements omit the bound slots and include requirements of the providers themselves. The binding's lifetime and retirement effects are part of the wrapper. Its raw remainder is not publicly extractable.

A suspended running computation retains all installed inner bindings. Shallow observation removes only its selected boundary. An unbound reply can be driven under explicitly supplied compatible outer bindings; no hidden promise of policy preservation exists. A bound computation's wrapper reinstalls its policy, budget and revocation state at every drive.

An escaping callable does not automatically inherit the handler around the code that constructed it. To retain that policy, bind the returned callable/computation explicitly. Task libraries accept closed or appropriately bound jobs. They do not silently import the scheduler's stronger authority.

11. Ownership, borrowing, and callable modes

Source ownership is affine: zero or one consuming uses. Runtime obligations remain linear: each owner is transferred, retained by an explicit live root, or retired once. An unused owner elaborates to disposal at its defined scope boundary, not to deletion of its existence.

Copy is a compiler-validated structural property. Copy values have no observable destructor or independent resource obligation. Nominal opaque types export Copy only through validated evidence from their defining scope. Fn does not imply Copy. Clone is an ordinary effectful callable returning another owner.

The three invocation modes are:

Fn can be used through exclusive or consuming invocation; FnMut through consuming invocation. No conversion duplicates the callable. A reusable call can still perform effects. Its environment loan persists until its execution finishes or retires, including suspension. Overlapping FnMut invocations reject. Send and Sync are independent validated capture properties.

mut counter = 0
increment = fun() { set counter += 1 }
// increment is FnMut and borrows counter exclusively for its capture lifetime.
repeat_calls(3, set increment)

consume_once = fun() { consume(own resource) }
// consume_once is FnOnce; repeating it is rejected.

Capture defaults are inferred from uses: Copy reads snapshot; immutable affine reads borrow; mutations borrow exclusively; ownership-consuming uses move. own capture clauses can force move capture. Reassignment requires mut even when the binding owns its value.

Loans are scoped access values in the core: Ref(r,A), Mut(r,A), and Init(r,A). Ordinary syntax primarily uses access modes. Their captures retain outlives constraints. Borrowing across capture is permitted when storage is stable and incompatible access remains excluded. A frame that must remain address-stable is pinned by its region ownership; pinning is not arbitrary shared mutation.

Disjoint static fields can be borrowed independently. Dynamic projections conservatively overlap unless a checked split operation returns separate permissions. A loan may end at its last use if no later access or dependent capture needs it. This does not move observable owner destruction. A request with read/mut payload access owns permission handles into stable producer storage. Its reply cannot rearm the producer while a conflicting payload-derived projection remains live. A response-lifetime contract must close or transfer these permissions before conflicting producer access. An exclusive lending cursor cannot advance while a projection is outstanding. No safe forget discards a loan or retirement obligation. Intentional leaks require an explicit detached owner whose region remains live; safe scope teardown cannot reclaim its backing storage.

12. Calls, preparation, and once-only results

Value parameters evaluate left to right to completed values. Computation parameters construct and prepare their argument expressions left to right to the first selected operation or completion. Unselected effects propagate immediately and suspend later argument preparation. Formal adjustment sets are known from the signature, not discovered by executing the callee body.

A block passed to a computation port is one execution; a callable is a value unless explicitly invoked. An already completed value is lifted into a completed computation without re-evaluation. A stored suspend { body } constructs a cold owned computation and transfers its captures immediately; it executes only when driven. The suspend form is optional explicit construction syntax over U, not a reusable closure.

repeat_value(3, { print("hi"); () })
// One argument evaluation, one print, three copies of Unit if the library repeats values.

repeat_calls(3, fun() { print("hi") })
// Three invocations, three prints.

cold = suspend { print("not yet") }

An adjusted argument may be prepared even if the callee later ignores it. A captured request may therefore be abandoned before receiving a response. Later arguments still prepare after an intercepted abort-like request; this is an intentional consequence of eager-to-interaction preparation. A lazy conditional must accept callables or explicitly cold inputs and drive only one.

An observation shape has computation leaves, ordinary-value leaves, and transparent product nodes. handle marks computation-typed leaves in its input product. It lifts ordinary leaves to completed values. ? on a transparent product uses the same left-to-right traversal. It does not inspect opaque storage or traverse a dynamically sized collection. Use an explicit finite traversal for those collections. @observe remains the single-leaf primitive. Thus a tuple can contain an owned producer and an ordinary number. Applying ? to that tuple observes the producer once. The subsequent match is ordinary tuple selection with operation patterns.

Prepared cells store either a completed value or one request and reply. Re-observation of a prepared cell returns its existing interaction without running it again. Rearming makes it runnable. There is no implicit repeated evaluation and no multi-shot continuation.

If argument construction fails partway, only constructed argument owners retire. Captures are acquired when their argument is formed, in source order, not all at once before earlier argument evaluation.

13. Observation and callable replies

job! executes to its final value, using supplied handlers. job? executes to one selected interaction. For a computation with interface adjustment H and residual row R, observation catches H and forwards R. observe(own job, H) is the explicit library spelling of the same checked primitive; H is CT-known. A naked ? uses the port's declared adjustment, not every effect in the universe.

mut job: Nat ~ Console = suspend { work() }
loop {
  match job? {
    ctl Console.Write(message) @ k {
      system_write(message)
      set job = k()
    }
    ctl Console.Read() @ k {
      set job = k(system_read())
    }
    result { return result }
  }
}

The explicit loop itself requires Tick unless a surrounding handler provides it. system_write and system_read denote supplied services, not globals. Their effects propagate from the arm.

k is a compiler-issued affine reply represented as a FnOnce callable. Its type returns Susp(OriginalResult, OriginalRequirements, SuccessorRetirement). SuccessorRetirement includes the retained segment and the installed response's retirement requirements. Capture and loan qualifiers also remain. This bound must fit any destination port or queue. Calling it consumes response and reply and constructs a runnable remainder. It does not execute that remainder. A Unit response allows k() as the Unit-argument convenience.

Reply construction has no user-visible allocation: it reuses the suspended segment and its reserved response slot. Validation occurs before either owner is irreversibly consumed. Compiler work accounting may still charge administrative work. Dropping a ready reply result also drops its installed response if unused.

Replies may escape when their owners, loans, service bindings and retirement effects permit. There is no scoped-resume keyword and no automatic deep interpretation attached to ctl. Deep behavior is an ordinary driver around the shallow remainder.

14. Match and handle: complete arm rules

match e { arms } evaluates e once and selects one arm. Matching itself does not execute arbitrary data. Observation is explicit through ?; port entry preparation is separately specified. For an observed type, ordinary patterns are lifted to the completed alternative. ctl Op(payload) @ k selects a request and binds its reply. _ can ignore any observed alternative. Explicit fully qualified Step.Done(value) and Step.Request(packet) patterns bypass the lifting and inspect the raw kernel sum. The latter binds an opaque payload-plus-reply packet, suitable for forwarding an abstract residual row. A closed selection must be exhaustively covered; an unknown intercepted tail needs a raw request fallback or an explicit narrower selection. Outside observed types, all patterns retain ordinary ADT meaning.

pair = (producer?, 7)
match pair {
  (0, 7) -> "zero"
  (ctl Log(message) @ k, _) -> consume_request(message, k)
  (n, _) -> format(n)
}

The request arm must return the same match result type as other reachable non-transferring arms. Consuming pair does not permit accessing a moved original producer. Nested ordinary enum patterns such as Some(value) introduce no reply obligation. Duplicate binders reject; repeated names do not imply equality patterns.

Patterns support wildcard, binder, literals, tuples, field-labelled constructor patterns, ordinary name @ pattern for non-owning inspection, and operation patterns. Ordinary whole-value @ cannot introduce two owning aliases: a whole binding is borrowed until any selected field moves, after which it is unavailable. In ctl Op(...) @ k, the postfix binder specifically denotes the reply field, not an alias of the payload.

Before selection, guards receive read-only views. Guards must have empty execution and disposal rows, be total under the admitted finite/structural rules, and neither move nor mutate the scrutinee or outer state. Guarded arms do not establish exhaustiveness. After selection, pattern-owned payload fields transfer. Unbound owned portions retire at arm exit after its result is protected.

14.1 Automatic operation patterns in one-shot match

fun Op(payload) hides the reply and uses the arm body to compute its response. In one-shot match, the arm's result is the rearmed input state, not the response and not automatic execution.

set job = match job? {
  fun Console.Write(message) -> system_write(message)
  fun Console.Read() -> system_read()
  result { return result }
}

For several observed ports, a fun-only request arm returns their successor tuple. Completed components are retained and request components are rearmed. A completed owned component may be read in the response computation but cannot also be moved out and retained in the successor state. That is an ordinary ownership error. A response product is Unit for zero requests, the response itself for one, and a tuple in left-to-right pattern order for multiple requests. In automatic continuing arms, ordinary completed-value binders are shared views of the retained completed cells; request payload bindings own their extracted arguments. An explicit move from a retained completed cell is rejected unless a control arm supplies a complete replacement state. Copy reads remain snapshots.

14.2 Repeated handling

handle e { arms } owns a tuple/tree of port cells. Each round prepares all runnable marked cells left to right, preserves cached completions/requests, then selects one arm.

handle (producer, optional_value) {
  (fun Get(), Some(value)) -> value
  (ctl Get() @ k, None) -> Result.Err(MissingValue)
  (result, _) -> Result.Ok(result)
}

A fun-only operation arm computes responses, rearms the selected ports, and repeats. A completed-value arm returns the handled result. A ctl-only arm executes normally and its result finishes this handle. It may use continue with new_state to replace the complete handler state and repeat. This statement is allowed only inside handle and elaborates to the ordinary Again constructor of the core driver action. continue without with means Again with the current complete state and rejects if any required cell has been consumed without replacement.

handle (producer, consumer) {
  (_, result) -> Result.Ok(result)
  ((), ctl Recv() @ waiting) -> Result.Err(())
  (fun Send(item), fun Recv()) -> ((), item)
}

Both ports prepare each round before any arm is tried. This pipe may perform one producer interaction before discovering consumer completion. It is not demand-driven pipe semantics. A consumer-first, no-prefetch pipe uses nested explicit observations instead.

14.3 Mixed automatic and explicit operation patterns

Mixed fun/ctl patterns are legal but cannot silently guess when the automatic responses become available. Their body constructs an ordinary After(answers, continuation) value. answers is the response product for fun patterns. continuation is an owned FnOnce receiving the rearmed automatic ports (one directly, several as a tuple). The driver computes answers, rearms those ports without executing them, then invokes the continuation. In handle this continuation returns the ordinary sum Decision(S,R) = Again(S) | Done(R) explicitly. It cannot use a lexical continue targeting a different function body. Ordinary completed cells that will survive are borrowed while answers are computed and are transferred into the continuation's successor-state environment exactly once.

handle (left, right) {
  (fun A(x), ctl B(y) @ kb) {
    After(answer_a(x), fun(own next_left) {
      next_right = kb(answer_b(y))
      Again((next_left, next_right))
    })
  }
  (_, result) -> result
}

After is a standard typed product of answers and a continuation, not a new control primitive. Its continuation has an ordinary function boundary and returns an ordinary decision value. In one-shot match, this continuation instead produces the ordinary match result and has no implicit repeat target. Done, Again and After in these contracts denote the compiler-selected standard declarations, not arbitrary same-named constructors; they have ordinary public construction paths. This makes (ctl A, ordinary_value) simple, while (ctl A, fun B) has explicit coordination order. All-ctl code remains the primitive alternative and can express the same behavior with ordinary reply calls.

15. Tick, finite iteration, and termination summaries

Every while, loop, and potentially recursive call cycle receives Tick checkpoints. The compiler computes SCCs of the resolved call graph and conservatively checks each recursive internal call edge. Indirect callable contracts carry Tick or Diverge unless a checked total-invocation certificate excludes unbounded internal recursion. The certificate records transitive callable dependencies. Those dependencies must be stable and well founded. Loading future call targets through mutable callable-containing state does not establish such a certificate. Passing that target through a helper does not remove the dependency. The checker inserts a conservative Tick or rejects an incompatible closed row. This prevents mutable higher-order recursion from acquiring a false pure contract. Ordinary FnMut closures that update scalar state can still have total-invocation certificates. Unresolved recursion cannot be assumed absent.

A checkpoint precedes each selected recursive call edge. For while, the initial condition executes first. A true condition enters the first body without a backedge checkpoint. Normal body completion or continue executes Tick before returning to the condition. For loop, normal body completion or continue executes Tick before returning to the body start. Break and return do not execute that backedge Tick. These rules permit initial finite work before the first checkpoint. This is a semantic operation, not necessarily a runtime allocation. A known always-continue handler can erase it; a tick counter can compile to arithmetic and a branch.

for requires FiniteIterator. This is a sealed traversal protocol: a private remaining-rank token decreases on each permitted next step, and exhaustion terminates iteration. User iterator implementations receive a finite allowance through a checked constructor and cannot reset it; early exhaustion is allowed. A size hint or double-ended API alone is insufficient. The iterator's body/next effects still propagate, so a finite number of calls to divergent next does not imply termination.

Tick limits count checkpoint crossings, not total work. A tick-limit driver uses a finite allowance iterator and one-step observation. It does not need another Tick handler for its own loop. It allows the configured number of Tick responses and one final observation that either returns completion or aborts on another Tick. The allowance representation handles Nat's maximum without arithmetic overflow.

An unrestricted structural driver that repeatedly answers Tick introduces the behavioral marker Diverge. This is checked by the core driver rule: interpreting the cycle-breaking Tick with unlimited Again has no finite-rank certificate, so its outward summary includes Diverge. A finite-rank driver can discharge Tick without Diverge and expose Abort on exhausted allowance. Structural drivers for other operations inherit the termination summary of their input and clauses; their administrative dispatch is not a new user loop requiring Tick.

tick_limit: Nat x Susp(A, Tick + E, K) -> F_(Abort + E + K) A
allow_divergence: Susp(A, Tick + E, K) -> F_(Diverge + E + K) A
// With empty K, these have the simpler Abort + E and Diverge + E contracts.

Interpreting execution requests does not automatically interpret disposal requests. A handler that abandons a port must account for K at that point. Bind cleanup providers into the resource when the release policy must survive handler changes. A tick limit cannot promise bounded cleanup whose own declared requirements permit unbounded work.

Diverge has no request payload, response or handler variant. Unknown blocking foreign work carries an appropriate external-wait requirement and, if it can run internally forever, Diverge. Removing Diverge requires a checked bounded-evaluation boundary or a valid totality derivation, not row subtraction.

Compiler-stage budgets charge evaluator instructions, dispatch, primitive bulk work, type normalization, reflection walks, allocations, generated nodes and nested calls against inherited counters. Tick erasure does not erase accounting. Native compiler providers require separately enforceable contracts. Budget exhaustion is a compiler diagnostic, not a user-handler event that can reset the budget.

16. Mutation, places, and projections

A place is a typed path into initialized storage, paired with permission. Field selection does not invoke arbitrary user code; indexing a user container calls its declared projection interface. Address calculations evaluate once, outermost to innermost. Each bounds check precedes the next index and the RHS. Mutation checks existing loans before evaluation proceeds.

An index field used by another field's type becomes immutable when the aggregate is published. A mutable borrow of the aggregate does not permit changing that index alone. To change it, consume the aggregate and construct a new checked dependent package. Private builders may update an index before publishing the fields that depend on it.

For replacement, evaluate and protect the new value. Atomically swap it into the initialized destination. Then retire the old owner. If retirement aborts, the destination still contains the new value. The mutation is committed; it is not rolled back. This order keeps borrowed aggregates valid when cleanup fails. It deliberately differs from the earlier replacement proposal. swap returns the old owner without retirement. Compound assignment takes a Copy snapshot before RHS evaluation. It applies the checked operator before the swap. Failure before the swap leaves the destination unchanged.

Initialization places cannot be read before initialization. Initializing an already initialized slot rejects or raises Abort according to whether the state is statically known. Partial construction owns its initialized children. Publication is a separate checked transition.

A lending generator yields a permission-bearing place with a reply gated on closure of its loan. A projected mutable place and its producer cannot run concurrently. Runtime checks may establish disjointness, but never manufacture lifetime. The conservative implementation can borrow a whole container while one element is projected.

for set element in list.places() {
  set element += 1
  Console.Write("updated")
}

The loan survives Console suspension. Cancellation retires the consumer's projection first, then the producer/container. Appending obtains a source value before reserving an initialization slot; publishing length follows successful initialization. Self-extension with conflicting loans rejects unless the user explicitly snapshots or selects a separately checked algorithm.

17. Cleanup order and normal return

Destruction has an ordinary custom computation followed by mandatory retirement. Effects of both belong to DropEffects(T) and to every scope exit that may execute them. A destructor uses stored authority, not a newly found ambient provider for the resource it is obligated to release. Additional outward effects must be declared and available at the retirement site.

Exact order:

1. Remaining statement temporaries: reverse creation order at statement end.
2. Remaining locals: reverse declaration order when their scope exits.
3. Parameters: reverse declaration order after body locals.
4. A custom destructor: before remaining owned fields.
5. Record fields: declaration order; tuple/array fields: increasing index; enum fields: active variant declaration order.
6. Captured continuation frames: innermost to outermost, with each frame following these rules.

Moving clears the source initialization bit. Partial values retire only initialized children and do not run a full-object custom destructor. Partial moves from a type with custom destruction require an explicit checked replacement/extraction API; arbitrary field move-out is rejected.

Temporaries are not implicitly lifetime-extended beyond their full statement. Bind a local explicitly to extend storage lifetime. Backing storage must remain valid while a loan or operation can access it. Unused plain loan permissions can close before owner destruction without running user code. If user destructors need a dependency order that conflicts with the specified source order, reject the program. Require an explicit earlier drop or a different enclosing scope. Do not silently reorder observable destructors. Pending external operations retain their backing region under the registered scope obligation until safe completion.

Return evaluates and protects its result, retires the departing scopes, then publishes the result. Either a protected caller slot or a local return slot is valid. The caller cannot observe a successful result before required cleanup completes. If cleanup changes success into failure, the protected result is also retired. break and continue perform the same cleanup for exited scopes.

fun ordered(own first: Resource, own second: Resource): Nat {
  own local = acquire()
  7
}
// Protect 7; retire local, second, first; publish 7.

The example's execution/retirement requirements are inferred if private; a public signature must declare them. No automatic destruction is silently assumed pure.

17.1 Declaring a destructor

A defining scope may attach one destructor before publishing its nominal declaration:

drop File(mut self): () ~ CloseFailure {
  set self.close_owned_handle()
}

This syntax supplies DeclarationSpec.destructor. It is not an unrelated extension method or a name-based convention. The body is checked as exclusive access to the complete value, with Unit result. It may suspend under the normal loan rules. It may use stored providers and persistent constants. It cannot move or return self. Field extraction requires a checked replacement operation. Mandatory field retirement follows the custom body, including its failure path.

An unrelated scope cannot replace a published destructor. A derive can supply one only through a declaration-building grant from the defining scope. A type with observable custom destruction cannot acquire Copy evidence. Arrow and brace destructor bodies have the same meaning.

18. Abort, Panic, and cleanup failures

Abort.raise(error): Never is a non-resumable recoverable operation. A normal handler can abandon its continuation and produce a result. Abort does not intrinsically poison a task. Bounds, checked arithmetic, invalid construction completion and explicit assertions use typed Abort errors unless a Result-returning primitive is selected.

Panic.raise(info): Never is a protected task-failure operation. It marks the current task poisoned and transfers control to its retirement supervisor. Only the task boundary supplies its protected binding. This uses a general binding rule: an owned provider may seal a slot against rebinding and outside observation. The binding contract records that permission. Ordinary observers cannot select the task's sealed Panic slot or shadow it with an implicit argument. They cannot intercept Panic inside the task and resume application execution. A supervisor receives the final report and may start fresh work. Panic is not permission for undefined behavior.

A retirement supervisor maintains a report containing primary, an ordered list of secondary cleanup failures, and poisoned. Primary is the first abnormal event (Abort, cancellation or Panic). If normal completion first fails in cleanup, that failure becomes primary. Any Panic sets poisoned even when another primary already exists. The original panic point is never resumed.

Each cleanup action runs under a retirement boundary that catches Abort/Panic, records it, and continues mandatory retirement of remaining fields/obligations where possible. Public drop/@retire returns Unit only on successful retirement. After safe retirement, an explicit drop that encountered Abort propagates a cleanup-failure Abort; a Panic still poisons the task. During scope unwinding the enclosing retirement supervisor accumulates these outcomes rather than reentering ordinary source code. Its internal report is not a normal successful return from a failed drop. If an external release cannot establish safe completion, its pending record remains owned; a report cannot claim completed retirement. A finalizer may diverge if its declared effects permit it. No liveness guarantee is invented.

A poisoned task does not automatically poison every shared service it touched. A service either restores its invariants before external reentry or has its own explicit poisoning protocol. No automatic rollback of logs, network messages or accepted commits occurs.

Process destruction, host crash and deliberate host fail-stop termination are outside successful cleanup guarantees. They are not implicit alternatives used to implement an ordinary checked source error.

19. Async operations and cancellation

A task has Running, CancelRequested, Retiring, and Finished states. Cancellation is sticky and cooperative. Checkpoints include explicit cancellation checks, supplied Tick policies, yields, and cancellation-aware external waits. Finite loops are not forced to check merely because they are long.

Cancel requests do not assert that execution stopped or resources were released. Join completes only when the task's result and required retirement are complete. Cleanup masks cancellation delivery but may suspend; repeated cancellation does not discard cleanup continuations.

Before host acceptance, the submitting task owns operation inputs. At acceptance, a pending-operation record owns any retained buffers, callback environments and completion correlation. Cancellation of the waiter does not free that record. Completion or acknowledgment that the provider will no longer access the resources permits retirement. A timeout alone is not such an acknowledgment.

Operation IDs include store identity and generation. Duplicate/stale completion is rejected before ownership transfer. If completion races with cancellation, one serialized acceptance/publication history determines the winner. A late owned result is first registered in the pending record, then delivered or retired; it never exists in an ownerless gap.

A group owns its child tasks. Normal exit waits for them; exceptional exit requests cancellation of all children before awaiting any one, then awaits safe retirement. A Join owns the right to consume a result; dropping it does not cancel a group-owned task. A standalone task must transfer supervision explicitly or cancel/join during its own disposal.

A scheduler queue owns rearmed computations, not running or unanswered ports. Reusable FnMut tasks cannot overlap invocation loans. Thread transfer requires Send for all captured state and appropriate sharing evidence for borrowed data. Ordinary Rc is not Send. Shared mutable state requires a checked synchronization protocol, not merely a shared pointer.

20. Protocol library contracts

These are ordinary library implementations over the core, not additional intrinsic execution models.

State/exception nesting remains observable. A state handler outside attempt can return updated state alongside Err; abandoning a state-owning computation inside an outer attempt retires that state. Neither operation undoes external effects.

21. Formal core: syntax and contexts

The following is mathematical notation. Surface declaration syntax elaborates to this kernel.

s ::= CT | RT
q ::= 0 | 1 | w                 erased, affine, unrestricted usage
m ::= Read | Mut | Own
j ::= Fn | FnMut | FnOnce

A,B ::= Ui | 1 | 0 | Scalar(t)
      | Pi(x:A).B | Sigma(x:A).B | Eq(A,v,w)
      | D(v*) | A tensor B | A plus B
      | Ref(r,A) | Mut(r,A) | Init(r,A)
      | U^chi(F_E A)
      | Callable^chi_j(P, F_E A)
      | Reply^chi(p, R(p), A, E)
      | Code(K,G,Contract)

E ::= (named request slots ; behavioral markers ; optional row tail)
chi ::= (owned captures, loan regions, service bindings, preferred observation selection,
         DropEffects, Send/Sync facts)

v ::= x | constant | constructor(v*) | pair(v,v)
    | pure_lambda x.v | thunk(M,environment)
    | closure(code,environment) | reply(segment,request_index)

M ::= return v | let x <- M in N | apply f(v*) | force v
    | perform slot.op(v) | observe_H v | rearm(v,v) | forward v
    | case v of arms | scope(L,M) | retire v
    | load p | move p | borrow_m p | end_loan l | initialize(p,v)
    | swap(p,v) | primitive(op,v*) | fix_tick f(x).M
    | finite_iter(iterator,body) | driver(certificate,state,round)
    | bind_services(bindings,v)

External await/cancel/task operations are ordinary authenticated service requests;
Await and task flags belong to the provider/machine semantics, not extra source forms.

P is a dependent port telescope, not merely a tuple type. Each port carries passing mode, value/computation classification and adjustment. Core rearm is a value-producing administrative computation whose public callable notation is k(v). It does not force its result.

Contexts:

• Signature S: nominal declarations, families, operation payload/response functions and implementations.
• Gamma: stable indices, CT values, unrestricted values and equations, each with stage and usage classification.
• Delta: ordered owned slots with initialization trees and destructor plans.
• Lambda: loans, place permissions and outlives constraints.
• I: named implicit values/providers and protected bindings.
• Q: pending response/initialization obligations.

Principal judgments:

S;Gamma |- A : Ui                         type formation
S;Gamma |- a == b : A                     pure conversion
S;Gamma |- chi valid                     capture/retirement validity
S;Gamma;I |- E <= E'                      requirement inclusion
S;Gamma;Delta;Lambda |-s v => A -| Delta';Lambda'
S;Gamma;Delta;Lambda;I;Q |-s M => F_E A -| Delta';Lambda';Q'
S;Gamma;Delta;Lambda |- p : Place(r,A,state,mode)
S;Gamma |- declaration valid
S;Gamma;I |- CT e evaluates to checked value v
S;Gamma;I |- persist(v,RT) valid

Elaboration produces core terms plus these derivations. Successful standalone checking does not certify an arbitrary fragment's later composition; free usage, scopes and effects must be rechecked when embedded.

22. Formal typing rules

22.1 Dependent formation and conversion

Gamma |- A : Ui       Indexable(A)       Gamma,x:A |- B : Uj
------------------------------------------------ PI / SIGMA
Gamma |- Pi(x:A).B : Umax(i,j)
Gamma |- Sigma(x:A).B : Umax(i,j)

Gamma,x:A |- b:B
------------------------------------------------ PURE-LAMBDA
Gamma |- lambda x.b : Pi(x:A).B

Gamma |- f:Pi(x:A).B      Gamma |- a:A
------------------------------------------------ PURE-APP
Gamma |- f a : B[a/x]

Gamma |- a:A     Gamma |- b:B[a/x]
------------------------------------------------ PAIR
Gamma |- (a,b) : Sigma(x:A).B

Gamma |- e:Eq(A,a,b)      Gamma |- v:P(a)
------------------------------------------------ TRANSPORT
Gamma |- transport(e,v):P(b)

Pure lambda rules apply to the stable index fragment, with no runtime effects, mutable access, or resource capture. Their dependent domain must be Indexable. This does not restrict ordinary owned products or executable callable domains. A dependent package can have a stable index and an affine payload. A resource can supply a stable brand without becoming an indexable owner. General executable functions use Callable and computation judgments. Refl constructs Eq(A,a,a); equality elimination is the ordinary identity eliminator. Universes are predicative and recursive data definitions are strictly positive. Recursive inline layouts reject independently of positivity; Box/Buffer indirection makes finite representation possible.

Conversion checks equal universe levels or an explicit cumulative universe lift, equal authentic nominal heads and convertible arguments, and normalized pure terms. It never reads effectful runtime state. A GADT match adds constructor equations to Gamma; its body is checked under those equations. Any dependent index escaping its scope must be returned in Sigma or be already expressible in the outer context.

22.2 Values, ownership and sequencing

x:A in Gamma; Copy(A)
-------------------------------- COPY
read x:A leaves contexts unchanged

x:A initialized in Delta; no incompatible loan
-------------------------------- MOVE
move x:A removes its initialized ownership from Delta

v:A transforms D0 to D1
-------------------------------- RETURN
return v:F_empty A transforms D0 to D1

M:F_E A transforms D0 to D1
N:F_R B under D1,x:A transforms to D2
x not free in outer result B, or explicitly packaged
------------------------------------------------ BIND
let x<-M in N:F_(E union R) B transforms D0 to D2

The dependent bind case packages a stable index and dependent result in Sigma when needed. It does not duplicate an affine x to place one copy in a witness and another in the result. Only an admissible stable index projection may be retained as erased metadata after its runtime owner moves.

Affine weakening is elaborated, not a pure structural equation:

unused x:A at exit; retire_A has requirements K
------------------------------------------------ WEAKEN-WITH-RETIREMENT
insert retire x at its ordered exit point; add K to outward requirements

Branch joins require compatible loans. A subsequently read owner must be initialized on every incoming path. An unused owner may have a conditional initialization flag after the join. Retain that flag until its original scope exit; retire it there only on paths where it remains owned. Do not insert an early drop at the join merely because no later read occurs. Branch-local owners still retire when their own branch scope ends. GADT refinement evidence is arm-local unless explicitly packed. Explicit failure paths must satisfy the same ownership accounting.

22.3 Closures, loans and invocation

A closure's free-variable analysis selects moves, snapshots and loans. Its chi records all retained dependencies. For Fn, capture use never requires exclusive access or ownership extraction. FnMut may exclusively access but must restore its environment on successful return. FnOnce transfers its environment. All modes retain valid cleanup plans on failure.

callee:Callable_j^chi(P,F_E A)
arguments satisfy P in source order
access to callee satisfies j; all captured loans outlive invocation
------------------------------------------------ APPLY
apply callee(args):F_(argument-effects union E) A

Borrow rules require initialized storage and disjointness when either access is exclusive. Suspension preserves Lambda; it does not clear it. Escape requires each retained region to outlive the destination. Ending a loan consumes its permission and restores parent access. A lending reply cannot rearm its producer until outstanding projected permissions close.

22.4 Operations, observation and replies

For operation i, payload type is P_i and response family is R_i(p):

p:P_i; inputs transferred or scoped according to signature
slot i available as request requirement
------------------------------------------------ PERFORM
perform i(p):F_{i} R_i(p)

The observed type is:

Step_H(A,E) = Done(A)
            + sum i in H. Sigma(p:P_i).Reply(p,R_i(p),A,E)

Sigma is an owned dependent pair: its first field stores p exactly once and its second stores the corresponding reply. Stable response indices are retained in the reply's request metadata even after payload extraction. These are immutable snapshots from request formation. Mutating a handler-local copy does not change the response type expected by that reply.

c:U^chi(F_E A); H subset of request slots(E)
------------------------------------------------ OBSERVE
observe_H c : F_(E minus H) Step_H(A,E)

Behavioral markers in E are never removed by request observation. Retirement of the observed event has its own K requirements, carried by its type and added where actually retired.

k:Reply^chi(p,R_i(p),A,E); r:R_i(p)
------------------------------------------------ REARM
k(r): U^chi'(F_E A)

This consumes both owners, adds r to the capture state, and performs no body execution. A Never response has no valid argument. Forwarding an opaque residual request performs that request in the outer environment and returns its rearmed original remainder; it never automatically runs it.

22.5 Cases, drivers, retirement and effects

A case checks payload/refinement binders and requires common result type and compatible output contexts. Matching transfers ownership only after a true guard. Fun patterns elaborate to reply application; ctl patterns expose that application capability. Their surface arm rules in section 14 determine whether the result is successor state or a handled result.

A handler round has core type:

round : Own S -> F_E (Done(R) + Again(S))

driver(cert,s,round) iterates this action. The certificate is either finite rank, structural interpretation of input computation, or unrestricted. A finite rank must decrease before Again. Structural interpretation accounts for the input's Tick/Diverge behavior and cannot reintroduce an already consumed reply. Surface continue with is allowed only across scopes within the same handler-arm function boundary; it elaborates to Again, never a cross-function jump. Unrestricted repetition introduces Tick or, after an always-continue policy, Diverge. The certificate is checked evidence, not a user Boolean.

v:A; destructor/captured obligation plan requires K
------------------------------------------------ RETIRE
retire v:F_K Unit

The scope supervisor's internal DropReport is complete only when mandatory retirement has completed. Public retirement returns Unit on success or propagates the recorded failure under section 18; it does not turn Panic into a success value. Requirements of user cleanup and pending external work are not erased by reporting a failure. Effect inclusion uses named slot identity, response-family equality and marker inclusion. Handler subtraction removes only the slots actually intercepted; provider and clause effects are added. Public code cannot remove Diverge or protected task effects by constructing a row descriptor.

22.6 Staging

Gamma;I_CT |- e:F_E Type(i); providers satisfy E
bounded evaluation yields validated A:Ui
------------------------------------------------ TYPE-POSITION
e may elaborate to A in a type position

Open stable indices use symbolic formation, not backward runtime evaluation. Persistence requires a closed serializable value or code with explicitly modeled runtime free variables and no forbidden CT captures. CT authority does not persist merely because a generated callable mentions the same service name.

23. Denotation: trees, interpreters, and typed stacks

Ignoring resource accounting temporarily, define partial interaction trees over a dependent signature:

T_E(A) = bottom
       + Return(A)
       + sum i in E. Sigma(p:P_i).(R_i(p) -> T_E(A))

The sum includes requestable operations only. Behavioral markers constrain admissible trees; they are not extra request nodes. Infinite internal behavior requires an allowed divergence interpretation. The arrow is the extensional image of an affine continuation; the typed language cannot duplicate it. This set/domain interpretation intentionally forgets resource identity and is not by itself an ownership proof.

bind(bottom,f) = bottom
bind(Return(a),f) = f(a)
bind(Request(i,p,k),f) = Request(i,p,lambda r.bind(k(r),f))

observe_H(Return(a)) = Return(Done(a))
observe_H(Request(i,p,k)) = Return(Event(i,p,k))       if i in H
observe_H(Request(i,p,k)) = Request(i,p,lambda r.observe_H(k(r))) otherwise

rearm(k,r) denotes the suspended tree k(r), not its execution in the caller.

CBPV distinguishes carrying that denotation as a value from running it. Implementations need not materialize a tree or evaluate the continuation function at rearm time; they store its response and program counter.

A shallow clause receives k itself. A deep interpreter is derivable:

H(Return(a)) = return_clause(a)
H(Request(i,p,k)) = operation_clause(i,p,lambda r.H(k(r)))

Affetto's default ctl does not install the lambda r.H(...) wrapper. A deep driver may explicitly construct it using ordinary callable/computation factories. No multi-shot control follows from the mathematical function notation.

A program-wide call signature is a GADT Call(R) whose constructors contain invocation inputs and select their result type. Then:

Program(A) = Return(A) + exists R. Call(R) tensor (R -> Program(A))

Implementations expand Call(R) to Program(R). A typed stack Stack(A,Z) accepts an intermediate A and ultimately produces Z. Its frames contain A -> Program(B) and Stack(B,Z). Defunctionalizing these arrows yields enums of captured fields and code labels. Computation arguments make the signature higher order. A suspended multihandler retains several contexts; there need not be one global native call stack.

24. Resource-aware operational semantics

A machine configuration is:

<W, task, M, K>
W = (heap, owner graph, regions/loans, service bindings,
     scope ledgers, pending operations, task states, diagnostics)
K = sequencing frames | call frames | observation boundaries | retirement frames

Each heap allocation has store and generation identity. Each resource has exactly one current owning edge or an explicit pending/retirement root. Loans are non-owning edges with retained backing lifetime. Shared ownership libraries own control blocks and account their edges explicitly.

Representative transitions, omitting unchanged W:

<let x<-M in N, K> -> <M, Bind(x,N)::K>
<return v, Bind(x,N)::K> -> <N[v/x], K>
<force(thunk M), K> -> <M,K>
<observe_H c,K> -> <force c, Boundary(H,id)::K>
<return a, Boundary(H,id)::K> -> <return Done(a),K>

First resolve the request's authenticated binding. A sealed provider receives its request without interception by an outside observation boundary. For an interceptible selected request, split K into inner segment Ki, selected boundary, and outer Ko. Detach Ki into an affine reply and remove only that boundary. Inner boundaries stay in Ki. Return the event to Ko. For a residual request, traversal continues outward while retaining the waiting observation state in the captured continuation.

<perform i(p), Ki ++ Boundary(H,id)::Ko>
    -> <return Event(i,p,Reply(Ki)),Ko>                  if i in H

<apply Reply(Ki) r, K>
    -> <return Ready(Ki,response=r),K>

<force Ready(Ki,response=r),K>
    -> <return r, Ki ++ K>

Rearm is not the third transition; only force/observation attaches Ki to the current caller. Moves update initialization metadata atomically with ownership transfer before any later user effect can observe the state.

A source return creates a protected outcome and enters retirement frames. Retirement invokes custom destruction, records failures, visits initialized children in the specified order, and reclaims storage only after its external access obligations are discharged. No ordinary statements after a canceled suspension execute as cleanup.

External operation traces include Accept(o), CancelRequested(o), Complete(o,result), CancelAcknowledged(o), and Retire(o). Transitions validate generation and current state before consuming inputs. Completion publication and cancellation acceptance are serialized. A provider cannot be considered safely canceled merely because a timeout occurred.

Task cancellation changes the task flag. Delivery at a checkpoint enters retirement. Panic enters retirement with poisoned set. Retirement masks cancellation delivery but not recording. A stalled release retains its root and prevents Finished; it does not manufacture a success report.

25. Trace semantics and valid optimization

The full denotation is a resource-aware resumption over worlds: Return, Request, internal Delay, observable Emit, external Await, and scope-intercepted abnormal outcomes. Interpret it over admissible schedules to obtain finite, infinite and blocked traces. The observable alphabet includes public service interactions, externally visible destruction, accepted transfers and specified failure outcomes. Private internal frame operations may be hidden only when no available provider can observe them.

Regular expressions are useful descriptions of some protocols, not a complete semantics for recursive, nested, dependent interactions. General traces may require pushdown structure or arbitrary resumptions.

Optimization preserves permitted observations, ownership outcomes and failure ordering under the declared provider assumptions. Same returned value is insufficient. Do not move destruction to last use or reorder prepared arguments. Do not replay a rejected pattern. Do not suppress required effects through invalid caching or checkpoint erasure.

Known response-only handlers may inline into direct calls. Known ctl handlers may compile to explicit branches/frames. The compiler should specialize the interaction representation before relying on C optimization; an opaque generic trampoline is not assumed to disappear automatically. Stable frame/loan and observable retirement contracts still apply to optimized code.

26. Scalars, storage, foreign code, and targets

Baseline scalars are Unit, Never, Bool, N8/N16/N32/N64, I8/I16/I32/I64, target-sized Nat/Int, F32/F64. Bool's identity comes from the selected standard declaration, not matching variant names. Integer operators check overflow, division by zero and invalid shift counts; failure raises typed Abort. Explicit wrapping operations are modular. No implicit widening occurs. Casts are checked unless truncation is explicitly selected. Comparisons return standard Bool/Ordering according to the operand contract.

IEEE floating operations may produce NaN/infinity. Disable fast-math; no cross-target bit-identical float promise is added. IEEE floats do not have reflexive Eq evidence. Float-to-integer conversion rejects NaN, infinity and values outside the destination's inclusive range before truncation. Scalar primitives have total Result-returning versions; surface checked operators unwrap through Abort.

Typed allocation uses explicit capacity/backing authority. Box denotes unique stable ownership, not per-object system malloc. Storage descriptors retain release authority. Frame allocation is also accountable: dynamically required frame storage needs Alloc or pre-reserved execution storage. Resource exhaustion becomes the declared failure path before publishing the frame; a reserved retirement path must remain valid for already-owned state. Administrative replies and observation boundaries use reserved frame storage. They do not make an unreported fresh allocation. Each acquired owner or frame reserves its mandatory retirement traversal record. Cleanup must not need a new allocation to remember an existing release obligation. User destructor code may allocate and fail normally. Direct native calls require a bounded activation-storage plan. Unbounded source recursion must not cause unchecked C-stack growth.

The baseline runtime has no safe ambient raw-pointer construction. Trusted native adapters use manifest-approved symbols and explicitly checked layout/retention contracts. A native call is a suspension barrier; no Affetto capture crosses arbitrary live C frames. An async adapter returns a pending-operation owner and later reports completion. Foreign callbacks are synchronous unless independently owned and registered through that protocol.

A native adapter's declaration is an assumption, not a sandbox against malicious C. Real isolation is required when that threat is in scope. Runtime approval never grants compile-time FFI execution.

Final delivery remains an amalgamated C99 header and a checked WebAssembly Component with WIT/Canonical ABI boundaries as in 009. Dynamic dependent values cross those boundaries only through explicit wire/descriptor representations; no opaque compiler type handle is a C ABI value. Ownership, initialized state and disposal must survive representation lowering.

27. Closed compiler-intrinsic catalogue

All compiler intrinsics use @. Names not in this section reject. Compiler handle types are sealed nominal declarations in the bootstrap signature. They are not extra unchecked TypeForm constructors. Other APIs, including reflection convenience functions, builders, codecs, Tick policies, modules and schedulers, are ordinary library values. These are semantic contracts, not a promise of one machine instruction per intrinsic.

Notation: S is an authenticated construction scope; CT entries require the named compiler provider. Result-returning validation failures preserve input ownership unless explicitly marked consuming. Kernel failure is never permission to publish unchecked Type or Code. Every intrinsic has compiler-budget charges in CT, regardless of its language-level row.

There is no @resume, unchecked type cast, forge-fact, disable-checker, global environment lookup, raw AST execution, or arbitrary backend instruction escape.

27.1 TypeForm: complete constructors

Universe(level)
Unit | Never | Scalar(scalar_kind)
Product(fields) | Sum(alternatives)
Pi(binder,domain,codomain) | Sigma(binder,domain,codomain)
Identity(type,left,right)
FamilyApplication(declaration,arguments)
Reference(region,type,Read|Mut|Init)
Suspension(result,requirements,captures)
Callable(ports,peg,Fn|FnMut|FnOnce,captures)
Reply(request_family,payload_indices,result,requirements,captures)
Array(element,static_length)
Code(category,free_context,contract)

Type operands are closed Type handles or well-scoped TypeExpression fragments under an explicit index context. There is no free solver-metavariable handle. Only validated factory/declaration/primitive handles can appear in these forms. FamilyApplication instantiates a declared descriptor; Product/Sum are structural unless wrapped by @declare. Recursive references are legal only through @group placeholders until publication. Source structural tuple/array constructors use these same forms. Suspension and Reply forms describe types; they cannot construct a live continuation.

27.2 DeclarationSpec and alternative schema

DeclarationSpec {
  static_parameters, alternatives, associated_members,
  visibility, opacity, representation, destructor
}
Alternative {
  name, input_telescope, result_indices,
  response: None | DependentResponse,
  implementation: None | CheckedCode,
  visibility, source_span
}
Parameter {
  binder, type, CT|RT|Erased, Read|Mut|Own,
  Explicit|Implicit(slot), Value|Port(adjustment)
}
Peg { result, requirements, capture_constraints }

Origin is injected by @declare/@group from their authenticated scope/site and static arguments; it is not an editable DeclarationSpec field. No response means completed data. A responding alternative without an implementation needs external interpretation. No custom destructor means structural retirement. No representation annotation means canonical language layout, not C ABI. Associated members are ordinary dependent record members. Duplicate names in one namespace reject. A constructor's result_indices must instantiate its own declared family and satisfy universe/positivity checks.

27.3 DraftSyntax: all categories and nodes

Categories are TypeExpression, ValueExpression, Computation, Pattern, Declaration, Module. Construction does not execute the represented code.

Literal(type,value) | Reference(binder,access)
PureLambda(binder,domain,body) | PureApply(function,argument)
DependentPair(index,value) | DependentElim(pair,index_binder,value_binder,body)
Refl(type,value) | Transport(family,evidence,value)
Induction(family,motive,scrutinee,branches)
Construct(alternative,arguments) | Project(receiver,field)
Lambda(ports,peg,body,capture_policy) | Suspend(body)
Call(callee,arguments,implicit_overrides)
Return(value) | Sequence(binder,first,rest)
Block(items) | Scope(owned_bindings,body)
Case(scrutinee,arms) | If(condition,yes,no)
Loop(label,body) | While(label,condition,body)
For(label,iterator,pattern,body)
Break(label,value) | Continue(label,state_option)
Local(binder,mutable,initializer) | Assign(place,value) | Swap(place,value)
Borrow(place,mode) | EndLoan(permission) | Move(place)
Perform(slot,operation,payload) | Observe(job,selection) | Force(job)
Rearm(reply,response) | Forward(packet) | Retire(value)
Handle(inputs,arms) | BindServices(bindings,job)
Comptime(body) | Embed(checked_code)
Primitive(intrinsic_name,arguments)
Declaration(spec) | DefinitionGroup(specs) | Module(exports)
PatternWildcard | PatternBind(binder) | PatternLiteral(value)
PatternConstructor(alternative,fields) | PatternTuple(patterns)
PatternAt(binder,pattern) | PatternOperation(Fun|Ctl,operation,payload,reply_binder)

PureLambda/PureApply/Refl/Transport and the strictly-positive family's generated Induction eliminator are the explicit proof/index-building path; ordinary code need not use them for checked builders. Induction exposes recursive hypotheses only at the family's structurally smaller recursive fields, and its motive/branches are checked under their constructor equalities. Each constructor carries source/expansion provenance supplied by its scope. Case arms contain pattern, optional guard and body. Default capture policies use section 11. Local/control labels are authenticated binders, not strings. The checker rejects wrong categories, escaped binders, missing responses, undeclared effects and invalid ownership exactly as for surface syntax.

27.4 ScalarOp

The closed ScalarOp tags are:

AddChecked, SubChecked, MulChecked, DivChecked, RemChecked, NegChecked,
ShiftLeftChecked, ShiftRightChecked, WrapAdd, WrapSub, WrapMul,
BitAnd, BitOr, BitXor, BitNot, Equal, PartialCompare,
IntCastChecked, Truncate, FloatCast, FloatFromInt, IntFromFloatChecked, BoolNot

Boolean short circuit is If, not eager scalar application. Literal parsing is checked construction of Literal, not an unprivileged host-parser escape. Each tag validates operand types and target widths; ScalarError is Overflow, ZeroDivisor, InvalidShift, OutOfRange, or UnsupportedDomain. Surface operator wrappers convert selected errors to Abort. Structural equality is generated from validated field operations, not an arbitrary memory comparison.

27.5 MemoryOp

The closed tags are Layout, Allocate, Release, ProjectField, ProjectIndex, SplitChecked, BorrowRead, BorrowMut, EndLoan, Initialize, ReadCopy, MoveOut, Swap, Publish, FinishBuilder, ExposeForeign, RevokeForeign.

Allocate consumes explicit backing permission/capacity and returns Result(typed uninitialized storage, AllocError). Release requires no live initialized children or external leases. Project operations validate identity, layout and bounds. Borrow tags enforce exclusion. Initialize requires Init permission; ReadCopy requires Copy; MoveOut requires an allowed initialized owner and leaves a hole; Swap preserves initialization. Publish/FinishBuilder validate completeness before producing the public owner. ExposeForeign is available only in an approved adapter and creates a scoped retention record; RevokeForeign requires completion evidence and ends it. No ordinary integer becomes an address or permission. Mutation/read tags are stateful core primitives but do not acquire external authority; allocation and external exposure carry their declared service requirements. Failures return structured errors before changing ownership, except an already-started retirement has the explicit partial-state rules of section 17.

28. Reflection schema and hygiene

@describe returns one of these immutable views:

TypeInfo:
  Universe | Unit | Never | Scalar | Product | Sum
  DependentFunction | DependentPair | Identity
  Nominal | FamilyApplication | Reference
  Suspension | Callable | Reply | Array | Code | Opaque

DeclarationInfo:
  origin, static_parameters, authorized_alternatives,
  associated_members, representation, destructor_contract, visibility

FieldInfo:
  owner_type, field_handle, name, ordinal, dependent_type,
  passing_mode, stage, visibility

OperationInfo:
  interface_identity, operation_handle, payload_telescope,
  response_family, requirements, implementation_contract

CallableInfo:
  ports, adjustments, peg, invocation_mode, termination_summary, captures, retirement

CaptureInfo:
  owned_types, regions, access_modes, bound_services,
  drop_requirements, Send, Sync

LayoutInfo:
  Static(size_bytes,alignment,field_layouts,destructor_schema)
  Dynamic(layout_function_contract)
  Unavailable(reason)

Schemas are versioned by the compiler API revision. Unknown future tags are not silently accepted by an old compiler. Public descriptions are inert data; editing them cannot issue validated handles.

Fact kinds are Copy, Send, Sync, Indexable, FiniteLayout, FiniteTraversal, TotalInvocation, PartialEq, Eq, PartialOrd, Ord, Persistent, ABICompatible and InvocationMode. Results are Proven(sealed evidence), Refuted(reason), or Unknown(constraints). User predicates cannot issue these facts. A private type can export a validated contract without exposing its fields.

Reflection grants are scoped, attenuable and CT-only. An opaque type exposes identity and public contract. Its defining module may grant a derive access to selected fields without granting access to every private declaration. Compiler layout may be necessary for compilation internally without making that layout reflectively public.

Scopes and binders preserve hygiene. @binder(scope,key,hint) returns the same identity for the same explicit local key; conflicting reuse rejects. The hint never resolves a name. Generated references use handles; deliberate caller capture requires a supplied binder/context grant. A draft syntax value can be copied, but embedding two copies that consume one affine runtime variable is rejected by composition checking.

Code values carry category, free context, result contract, usage matrix, regions, stage and effect provenance. @check returns a checked fragment, not permission to bypass whole-program linking. @embed checks its free context at the insertion site. Recursive declaration groups publish atomically only after every body and layout is validated. No half-defined type is observable through layout queries.

29. Derivation examples and the complete metaprogram path

The standard reflect module is an ordinary implementation exposing typed wrappers over the intrinsic catalogue:

values(D): Type
operations(D): Type
requests(D,R): Type
observations(D,A): Type
fields(T,grant): List(FieldInfo)
alternatives(D,grant): List(AlternativeInfo)
lookup_field(T,name,grant): Option(FieldInfo)
query_fact(kind,args): FactResult

These wrappers require Reflect/Codegen as appropriate and preserve the authenticity of the handles they return. reflect.describe abbreviates @describe with the current explicitly supplied reflection grant. The grant parameter to fields/alternatives may be supplied implicitly. The fields operation requires one fully authorized completed-product alternative. The alternatives operation returns the authorized interface view and reports opacity explicitly. observations adds reply fields, while requests projects only request payloads and preserves their response index. Neither constructs a live reply. There is no automatic global derive registry. A policy record supplies codecs for primitive and opaque types and rules for recursive references.

29.1 A structural field-count factory

fun field_count(T: Type): Nat ~ Reflect + Abort {
  reflect.fields(T).length
}

This requests reflection while constructing its answer. reflect.fields requires an authorized product view and raises Abort.Reflection(NotARecord or Opaque) otherwise; it does not silently count a partial private representation. Its numeric result can persist; its reflection grant cannot.

29.2 Complete derive algorithm

derive_codec(T, policy, grant) performs the following deterministic algorithm:

1. Query T with the supplied grant. Reuse an explicitly supplied policy codec for opaque types; otherwise reject an opaque representation request.
2. For scalars, select the policy's explicit wire representation, not target-native bytes.
3. For products, enumerate authorized fields in declaration order. For each field, obtain its dependent type and codec in the context of preceding stable fields.
4. For sums, obtain stable explicit wire tags from policy. Reject duplicate tags. Do not serialize compiler ordinals or addresses implicitly.
5. Reserve recursive implementation identities in one @group transaction. Emit recursive calls rather than infinitely deriving recursive pointees.
6. Construct an encoder callable with a read port for T and the policy's writer port/requirements. Emit checked field projections and codec calls in wire order.
7. Construct a decoder callable with the reader port/requirements. Decode into a private builder, recording initialization after each field. Validate tags, lengths, indices and scalar constraints before publication.
8. For dependent fields, previously decoded stable indices specialize or instantiate the permitted runtime family. A representation requiring new CT computation from runtime input rejects; use the family's declared dynamic representation.
9. On decode failure, return a structured error and retire the initialized prefix. No partially decoded object has type T.
10. Check both generated bodies using @check. Then construct Impl(Codec(T)). Preserve source/derive spans. Publish only after every check succeeds.

A concrete Pair(Byte,Byte) encoder lowers to the equivalent of:

fun encode_pair(value: Pair(Byte, Byte), mut writer: Writer): () ~ WriteFailure {
  set writer.write_byte(value.first)
  set writer.write_byte(value.second)
}

Its decoder is equivalent to:

fun decode_pair(mut reader: Reader): Result(Pair(Byte, Byte), DecodeError) ~ ReadFailure {
  first = set reader.read_byte()
  second = set reader.read_byte()
  Result.Ok(Pair(Byte, Byte)(first, second))
}

For an owning field the generated decoder uses a builder so the first owner is retired if decoding the second fails. The example's reader contract reports input failure through ReadFailure. This pair has no malformed-value cases beyond byte reads. Its explicit Result is Ok on normal completion. A codec boundary can interpret ReadFailure into DecodeError. The derive never treats a successful Boolean predicate as a constructor permission.

29.3 Building without privileged syntax

For the encoder, construct a child scope, binders value and writer, and authorized field handles. Build DraftSyntax nodes Project(Reference(value),field), Call(codec.encode,...), and Sequence in field order. Wrap in Lambda with Read T and Mut Writer ports and the explicit peg. Call @check with that contract, then @embed into an implementation constructor. Exactly the same nodes arise from parsing the handwritten encoder. No surface-only field privilege or private AST mutation is permitted.

29.4 Schema-to-type and module construction

comptime schema = parse_schema(@input(schema_ref))
comptime Packet = derive_record_type(schema)
comptime packet_codec = derive_codec(Packet, wire_policy, packet_grant)

The schema bytes are an explicitly named immutable input. Generated identifiers obtain scoped handles; schema strings cannot capture private locals. A returned module is a dependent record containing Packet, its codec, constants and other implementations. Its runtime projection contains only persistable code and data, not compiler handles used to construct them.

30. Diagnostics and elaboration pipeline

Every effect, ownership and staging constraint retains provenance. The compiler reports the originating expression, the propagation chain, the rejecting boundary, and a concrete remedy when available.

E_STAGE_SERVICE: reflect.fields cannot run in this runtime context
  requires compiler reflection
  introduced in derive_codec -> inspect_record -> reflect.fields
  evaluate the derivation at compile time and persist its checked result

E_REQUIREMENT: this recursive cycle requires Tick
  visit -> descend -> visit
  declare Tick or interpret it in this function

E_RETIREMENT: leaving this scope must close connection
  closure requires Async.Await, unavailable at this boundary

E_REPLY_MOVED: reply k was already consumed here
E_LOAN_ESCAPE: queued computation may outlive buffer's storage
E_TYPE_IDENTITY: same spelling does not identify these nominal Array constructors
E_BUDGET: compile-time work allowance exhausted during generated-code checking

Other stable categories are E_CONVERSION, E_UNIVERSE, E_GADT, E_LAYOUT, E_INIT, E_MOVE, E_MATCH, E_GUARD, E_CAPTURE, E_AUTHORITY, E_FFI, E_SEND and E_PANIC_BOUNDARY. Diagnostics are inert bounded text; rendering escapes terminal control sequences. Reflection does not expose secrets through unrestricted diagnostics.

Pipeline:

immutable authorized source graph
 -> lexical resolution and authenticated scopes
 -> construction programs over the public intrinsic kernel
 -> bounded CT evaluation and specialization
 -> dependent type/conversion/row checking
 -> CFG initialization, move, loan and capture checking
 -> explicit retirement and checkpoint elaboration
 -> checked ANF/CBPV core
 -> handler/callable specialization and frame splitting
 -> target layouts and ABI validation
 -> C99 / WebAssembly Component emission

Core intrinsics do not recursively require another macro expansion to execute. Type checking and compile-time evaluation interleave under a fixed evaluator/checker. Unbounded polymorphic specialization produces a bounded diagnostic. Runtime recursion within one specialization remains ordinary Tick-accounted recursion.

31. Worked compositions

31.1 Sum a producer with implicit rearming

fun sum(own producer: Port((), Send(Nat), Send(Nat), ())): Nat ~ Abort {
  mut total = 0
  handle producer {
    fun Send.send(value) {
      set total += value
    }
    () -> total
  }
}

The operation response is Unit. The handle driver rearms and reobserves; no per-item deep handler frame accumulates. Producer residual effects and retirement requirements must be present in a generalized signature. This closed example assumes none beyond the shown ones.

31.2 An explicit shallow driver

fun drive(own producer: Port(Nat, Console, Console, ())): Nat ~ ConsoleBackend + Tick {
  mut current = producer
  loop {
    match current? {
      ctl Console.Read() @ k {
        set current = k(backend.read())
      }
      ctl Console.Write(message) @ k {
        backend.write(message)
        set current = k()
      }
      value { return value }
    }
  }
}

Each path that continues the loop initializes current. Returning retires any remaining owned state. The backend is a named implicit service supplied by ConsoleBackend. The loop's Tick is explicit; it is not confused with producer Console operations.

31.3 Reusable versus consuming callbacks

fun repeat_calls(count: Nat, mut each: FnMut() -> ()): () {
  for index in range(0, count) {
    set each()
  }
}

set each() gives the callable receiver exclusive access for this invocation. It does not add a user argument. The shown callback is total and effect-free. An effect-polymorphic version binds an explicit row parameter and propagates it. fun() { print("hi") } requires its output effect in that row. A callable consuming an affine capture cannot satisfy FnMut.

31.4 Round-robin scheduling

The scheduler owns a bounded ready queue. Pop one job, observe its Schedule request, and either retire its completion or rearm and enqueue it. Yield enqueues at the tail. Spawn needs two free positions after popping the parent: child and rearmed parent. On failure return the unstarted child in the response. Existing tasks remain ahead of both. Successful spawn enqueues child before parent. The scheduler's own unbounded dispatch loop requires a Tick/Diverge policy; cooperative fairness says nothing about a job that never reaches a scheduling point.

match job? {
  ctl Schedule.yield_now() @ k {
    ready.push(k())
  }
  () {}
}

Typed await adds completion slots and pending-operation ownership, not a different continuation mechanism. Queue bounds alone do not bound blocked tasks or stage-local buffers.

31.5 Compile-time Tick handling is not the compiler budget

comptime codec = tick_limit(1000, { derive_codec(Person) })

The limit counts the derivation's Tick checkpoints. Reflection walks and finite code generation consume the compiler's independent work budget even when no Tick occurs. An inner handler cannot reset that budget.

31.6 Negative programs

first = k(answer)
second = k(answer)       // E_REPLY_MOVED

mut n = read_runtime()
T = comptime Array(Byte, n) // E_STAGE: runtime value cannot drive CT layout

copy = fun() { consume(own unique) }
repeat_calls(3, set copy) // E_CAPTURE / invocation-mode mismatch

match opaque_value? {
  ctl HiddenOperation() @ k -> forged_reply(k)
}                       // E_AUTHORITY or E_MATCH; names do not forge requests

32. Conformance obligations and migration map

This sibling language changes the earlier design in these areas:

• Observation uses ?; force uses !.
• A callable reply rearms without execution.
• Adjusted arguments prepare implicitly.
• Loans can survive capture.
• Destruction can perform effects and suspend.
• Checked source errors use Abort, not fail-stop traps.
• Named implicit slots route services.
• Diverge records behavior without an operation constructor.
• Dependent indices and public descriptor/code construction share one checked core. Adoption must explicitly revise the authoritative specification and tests. Existing regression counts do not establish any of these features.

Required independent checks:

1. Surface/builtin construction pairs for every DraftSyntax and TypeForm constructor.
2. Type preservation, progress up to requests/failure/allowed divergence, and conversion soundness for the stable core.
3. Unique ownership through calls, partial argument construction, observation, reply, forwarding and cancellation.
4. No replay on failed patterns; eager LTR preparation and selected-arm-only moves.
5. No execution at rearm; no administrative frame growth in a tail-loop driver.
6. GADT response refinement, runtime indexed buffers, universe rejection and nominal-forgery rejection.
7. Exact cleanup order, protected returns, primary/secondary failure ordering and async retained storage.
8. FnMut exclusion through suspension; loan lifetime through erased/existential wrappers.
9. Tick SCC/indirect-call coverage, finite iterator ranks, no-op erasure and independent CT budgeting.
10. Reflection privacy, hygienic binders, checked generated ownership, stable origins and cache revalidation.
11. Native/core-wasm equivalence for values, defined failures, effect order, lifetime events and target layout.
12. Denial of undeclared build inputs, network/process access, compile-time FFI and authority laundering through code values.

These are evidence obligations, not proofs supplied by this document. A finite test suite cannot prove the full calculus sound. A mechanized metatheory or executable reference model should precede claims of formal verification.

33. Deliberate boundaries

The proposal does not include multi-shot continuations or implicit cloning. It has no extensional equality solver or global instance search. Compiler/parser plugins cannot bypass the kernel. Arbitrary runtime type-layout synthesis is excluded. Guards cannot perform effects. Live loan obligations cannot be abandoned safely. Host capabilities and schedulers are not ambient. Rejected programs receive diagnostics rather than an invented fallback semantics.

Raw source-level deep resume, use-binding syntax, chained trailing argument sugar and generative alias keywords are not part of this draft. Deep interpreters, factories, modules, codecs, task groups and pipelines are expressible using the stated core and libraries.

The goal is not that every compiler mechanism disappears into a library. The trusted kernel still implements binding, conversion, validated construction, ownership, staging, primitive representation and control transitions. The symmetry is that all public constructions use that same kernel and none bypasses it.

34. Complete rule coverage and representation contracts

This section defines the remaining checking and execution cases. It also states the conditions that a backend must preserve.

34.1 Rules for every core form

The checker uses synthesis for names, primitives, projections and applications. It uses expected types for lambdas, constructors with implicit indices and arm bodies. An unresolved ordinary metavariable causes a diagnostic. It does not start a search over arbitrary programs.

Closure and suspension construction may need storage. The core value constructor itself assumes that this storage exists. Source elaboration inserts any necessary allocation before construction. After target layout, the compiler rechecks inserted storage requirements against the source contract. It may not add an undeclared allocation or silently fall back to malloc.

Every code node in section 27 maps to one of these forms. Surface Return, Break and Continue select an existing lexical target and insert cleanup for exited scopes. They cannot cross a callable boundary. A source field projection uses the matching place rule or a checked dependent-record elimination. It never performs a method call implicitly.

34.2 Memory operation types

The notation Cell(r,T,s) describes storage with state s. Own, Read, Mut and Init describe permissions, not duplicate pointers. Result errors preserve their input owners unless the table states a completed transfer.

MoveOut is not allowed through an ordinary borrowed mutable cell. Use Swap or a container operation that preserves the public container invariant. An owned private builder may contain holes because it is not yet a public initialized value. The convenient finish wrapper retires an incomplete returned builder and raises Abort.Uninitialized. A fallible try_finish returns it for repair instead.

SplitChecked uses numeric range checks before issuing disjointness evidence. Failure does not partly split authority. A child permission cannot escape the parent region or bypass the join obligation. ExposeForeign cannot turn arbitrary integers into pointers.

34.3 Layout and erasure

Canonical product layout places fields in declaration order. Each field starts at the next multiple of its required alignment. The final extent is rounded to the maximum field alignment. A zero-field product has size zero and alignment one. Zero-sized fields still have distinct logical place paths.

Canonical sum layout has an unsigned tag and a payload area. Use the smallest baseline unsigned tag type that can hold all declared completed alternatives. Tags follow declaration order. The payload alignment is the maximum admitted payload alignment. Its extent is the maximum admitted payload extent. A static index may make an alternative impossible, but it does not renumber the remaining wire-independent internal tags.

Array stride is the rounded element size. Array(T,0) has no element storage and needs no element destructor or stored Copy/Send permission. It has size zero and alignment one. Nonzero inline arrays require a complete static element layout. All layout arithmetic is checked before publication.

These are language layouts. An explicit foreign representation uses the target's validated C ABI instead. Wire encoding is a separate codec policy. No default serializer copies native padding or enum tags.

Known closed instantiations may be specialized. Abstract-size existential values use indirect typed slots with compiler-issued layout/move/retirement descriptors. These runtime descriptors are not compiler reflection handles. They expose only validated execution operations. Associated CT types can be erased while the instance retains its required execution descriptor.

This permits runtime dependent packages without arbitrary runtime type synthesis. A generic runtime body can operate through its supplied representation contract. It does not need to evaluate an unknown compiler-stage type factory.

34.4 Normalization and termination certificates

A stable conversion term cannot perform an effect, mutate storage, inspect a capability or call an uncertified recursive definition. Pure induction is structural on admitted positive data. Scalar conversion primitives are total Result-returning functions. Closed effectful type expressions first execute in CT and then contribute their checked result.

An empty outward effect row alone does not certify a conversion term. A computation may internally handle effects or mutate an explicit argument. Conversion requires a separate pure-normalization derivation for the term. This prevents a bound logging service from entering type equality merely because its outward row is empty.

A finite-loop certificate proves a bound on calls to next, not a bound on arbitrary work inside next. The next implementation's requirements remain visible. The primitive @finite enforces its rank token. Its step callback cannot replace that token with a larger one.

An observation with no Diverge requirement cannot internally bypass all relevant checkpoints through general recursion. A residual external wait may still wait indefinitely. Its request is visible; it is not an unrecorded pure reduction. A compiler work limit must account for provider work separately where evaluator instructions do not cover it.

35. Additional worked checks

35.1 GADT refinement without a proof argument

fun evaluate(comptime T: Type, expression: Expr(T)): T ~ () {
  match expression {
    Expr.Natural(value) -> value
    Expr.Boolean(value) -> value
  }
}

The Natural arm checks under T = Nat. The Boolean arm checks under T = Bool. Both produce the declared T after the constructor refinement. The caller supplies T explicitly here. An implicit named CT parameter is an equivalent interface choice.

35.2 A runtime length is not a CT type computation

fun packet(n: Nat, heap: Heap): SizedBytes ~ Alloc + Abort {
  bytes = make_bytes(n, heap)
  SizedBytes(n, bytes)
}

The buffer family already supports a runtime length. No reflection or new inline layout is needed. The returned dependent record stores the length witness needed by later operations.

fun invalid_packet(n: Nat): () {
  comptime T = Array(Byte, n)
}

This rejects because an RT parameter cannot supply a CT layout dimension. The rejection does not prohibit Buffer(Byte,n) or a dependent pair containing it.

35.3 Explicit equality evidence

match @equal(Nat, left_length, right_length) {
  Some(equal_lengths) {
    converted = @transport(buffer_family, equal_lengths, buffer)
    consume(converted)
  }
  None -> report_length_mismatch()
}

The context supplies a pure family buffer_family(n) = Buffer(Byte,n). The buffer initially has the left length. The successful check permits transport to the right length. It does not copy elements or allocate a second buffer. The example's surrounding function must declare effects of consume, reporting and retirement. A callable result does not erase those effects.

35.4 A request and ordinary data in one pattern

handle (producer, optional_value) {
  (fun Get(), Some(value)) -> value
  (ctl Get() @ k, None) -> Result.Err(MissingValue)
  (result, _) -> Result.Ok(result)
}

Assume Get returns a Copy scalar. The Some binding is a read of the retained completed cell. It supplies Get's response without consuming that cell. On the second arm, unused k retires the producer remainder. The third arm finishes and retires the unused ordinary input. The whole handled result has type Result, not Get's response type.

35.5 Two manual replies in a loop

match (producer?, consumer?) {
  (_, result) { return Result.Ok(result) }
  ((), ctl Recv() @ waiting) { return Result.Err(()) }
  (ctl Send(item) @ kp, ctl Recv() @ kc) {
    set producer = kp()
    set consumer = kc(item)
  }
}

This fragment belongs inside a Tick-accounted loop. Both inputs prepare before matching. Both replies return computation values without execution. The next loop observation selects the next interactions. No deep handler frame is installed by either call.

35.6 Checkpoint limit without a recursive limit handler

mut current = input
for index in range(0, allowance) {
  match current? {
    ctl Tick.checkpoint() @ k { set current = k() }
    value { return value }
  }
}
match current? {
  ctl Tick.checkpoint() @ remaining -> Abort.raise(TickLimit)
  value -> value
}

The input port selects Tick and forwards its explicit residual row. The enclosing function propagates residual and retirement requirements plus Abort. It uses no unbounded loop. With allowance zero, it can still observe completion, but cannot answer a Tick. There is no allowance-plus-one arithmetic overflow.

35.7 Cleanup trace after committed replacement

set holder.resource = replacement

The trace order is:

Evaluate(replacement)
Swap(holder.resource, replacement)
BeginDestroy(old_resource)
EndDestroy(old_resource)

If old destruction aborts, holder.resource still owns replacement. Cleanup failure propagates after mandatory retirement of the old resource. Code that catches Abort cannot observe an uninitialized public holder.

35.8 Effectful derive versus generated effects

comptime person_codec = derive_codec(Person, wire_policy, person_grant)

The derivation requires compiler reflection, code construction and its declared construction failures. The resulting Impl(Codec(Person)) contains generated code and permitted captures. Its encode and decode methods require their declared runtime services. It does not carry person_grant into the runtime program.

35.9 Direct construction agrees with source syntax

For a generated field read, the construction program creates these nodes:

scope = child_scope(derive_site, field_key)
value = binder(scope, "value")
writer = binder(scope, "writer")
field_value = Project(Reference(value, Read), authorized_field)
body = Call(codec_method, [field_value, Reference(writer, Mut)])
function = Lambda(checked_ports, checked_peg, body, inferred_captures)
checked = check(scope, function, expected_callable_contract)

These names abbreviate the catalogue's scope/binder/syntax/check calls. They describe a construction program, not new compiler intrinsics. The checker performs the same field, mode, effect and lifetime checks as for a handwritten method call.

36. Controlled-English vocabulary and reading rules

This document uses STE100-style controlled English. Formulas, source code, API names and standard technical terms retain their exact notation. This is a writing policy, not a claim of certified dictionary conformance.

A normative 'must' is a requirement of this proposal. 'May' grants an implementation choice only when the stated observations remain unchanged. Examples are contextual program fragments. Their named domain services and types must be supplied by the described surrounding context. Mathematical metavariables and omitted derivation contexts do not introduce implicit source names.

37. References and evidence

• Current contract, reflective construction proposal, places/scoped effects discussion, memory and trust discussion, prior ports proposal.
• Frank: Do Be Do Be Do: ports, pegs, adjustments and multi-handling; this document chooses its own imperative and ownership rules.
• A tutorial implementation of a dependently typed lambda calculus and Hirrolot's small CoC implementation: small dependent cores, not implementations of the resource/effect extensions here.
• Paul Blain Levy, Call-by-Push-Value: value/computation separation.
• Rust destructors: ordering inspiration; this document explicitly adds effectful/asynchronous retirement.

The proposal's conceptual endpoint is:

Algebraic declarations describe possible interactions. Dependent types describe their contracts. Affine ownership carries their obligations. Shallow interpreters select the next action. Compile-time programs construct these items through the same validated interface.