Ownership, initialization, cleanup, declared effects, errors, and verification.
Core-0 Ownership, Effects, Errors, and Contracts
Status: normative
Ownership, initialization, and cleanup
C0-OWN-001 — Ownership forms. A bare class handle, user value, Box<T>,
and collection own their contents. Shared<T> is explicit reference-counted
ownership; Weak<T> is non-owning. Ref<T> is a shared borrow, Mut<T> an
exclusive borrow, and Raw<T> is usable only with the unsafe effect.
C0-OWN-002 — Explicit transfer. Moving a named non-Copy owner requires
move(value); a fresh temporary transfers directly. Use after move, double
drop, and partially moved use are rejected over the checked CFG. The bounded
Stage0 schema-1.8 pass admits whole-local move paths only; field moves and path
restoration are recognized as unsupported rather than approximated.
C0-OWN-003 — Lexical nonescaping loans. Core-0 permits many overlapping shared loans or one exclusive overlapping loan. Loans cannot be stored in fields, variants, results, or captured state. At joins, a loan remains live if it is live on any incoming path.
The schema-1.9 lexical loan record makes that rule executable for the selfhost
byte kernel. It binds a shared Ref, exclusive Mut, or byte Slice to an
exact origin place from creation through its last reachable use. It permits
many shared loans or one exclusive loan over an overlapping place. A move, replacement, or drop conflicts with every live overlapping loan; mutation also
conflicts with a shared loan. Reborrowing suspends the parent exclusive loan,
and joins take the union of predecessor liveness.
The catalog’s Array<Byte>.slice selector and exact Bytes.slice SDK facade
are two surfaces of one narrow loan-producing operation. They are the sole
compiler-known declared-result exception: their transient apparent result may
flow only directly into a caller-local loan tied to the receiver. No
source-defined message or other selector may return Slice; it is not
storable or onward-returnable and cannot enter Result, a field, a variant,
or a capture. The checked take API returns owned bytes instead. This rule
does not admit general returned borrows or written lifetimes.
C0-INIT-001 — Definite initialization. Every field and local is checked by
move path. An initializer establishes every field exactly once before Self
escapes. A partially initialized object is not observable. For the bounded
Stage0 record, every owned parameter/local is in exactly one of the states
uninitialized, initialized, or moved on each CFG edge. A join retains a usable
owner only when every reachable predecessor supplies the initialized state;
otherwise a later use is rejected.
C0-INIT-002 — Class allocation. A class initializer takes an explicit
Ref<Allocator<A>>, allocates the complete most-derived object exactly once,
and returns Result<Self, InitError<A, E>>. Base initialization reuses that
allocation. A = Never selects faulting allocation; E = Never declares no
domain initialization failure.
C0-DROP-001 — Elaborated cleanup. Deterministic cleanup is inserted on
every normal, error, and control-flow edge after ownership checking. Cleanup
uses reverse initialization order and the allocator provenance recorded at
construction. Core-0 source cannot observe an implicit exception unwinder. In
schema 1.8 every exit edge retains explicit cleanup operations for each live
owned record, including records whose fields make destruction runtime-trivial.
An owned path consumed by move is not also dropped. On a try error edge,
these drops run before construction of the fresh outer Err.
Schema 1.9 records cleanup for every reachable fallthrough and branch and for every return, try error, break, continue, loop backedge, and join. When incoming owner
states differ, predecessor-specific cleanup reconciles them before the join;
no backend chooses a drop implicitly. Aggregate drop visits initialized fields
in recursive reverse initialization order and releases each unique runtime
handle exactly once.
Assignment and growable-buffer mutation preserve the replacement rule in
C0-TYPE-004: a replacement is produced successfully before the old value is dropped. Only then may REPLACE_COMMIT drop and overwrite the old place. A
failed producer, bounds check, size check, or allocator call leaves the exact
old value initialized and observably unchanged.
Effects and recoverable errors
C0-EFF-001 — Closed declaration. Every message and initializer declares an effect set, including an explicit empty set. A caller’s allowed effects must contain every transitive callee effect. Effect checking does not replace capability-value checks.
C0-EFF-002 — Unsafe boundary. Raw memory and host operations not exposed by
a safe intrinsic require unsafe in both the lexical block and the enclosing
effect allowance. The selfhost-0 compiler source does not use this facility.
C0-ERR-001 — One recoverable model. Recoverable source-level failure uses
the closed Result<T, E> carrier. A nominal error declaration is the standard
form for a domain-error family, but E follows the owned payload rule in
C0-ERR-003 and need not itself be an error. Prefix try propagates the exact
error payload through the current message’s result carrier. Core-0 has no
throws, exception unwinding, implicit error unions, or resumable conditions.
C0-ERR-002 — Fault distinction. A language fault represents violated safety or selected numeric semantics and is not silently converted to a domain error. Cold-path error observation/routing may add trace context without changing the ordinary-return source model.
C0-ERR-003 — Canonical intrinsic result. Result<T, E> is an invariant,
compiler-provided closed carrier with exactly two variants in canonical order:
Ok(value: T) has tag zero and Err(error: E) has tag one. Both arguments obey
the finite stored-payload rules; in particular, E may be any finite owned
non-borrow payload type and is not restricted to a nominal error. Construction
requires the explicit forms Result::<T, E>.Ok(value) and
Result::<T, E>.Err(error); generic arguments are not inferred for this
descriptor construction. Result patterns omit generic arguments and derive the
exact T and E only from the scrutinee type. The two tags are canonical
artifact and reflection facts and cannot be overridden.
C0-ERR-004 — Exact try propagation. In a message returning
Result<U, E>, the operand of try must have exact type Result<T, E> and is
evaluated exactly once. Ok(value) makes the expression produce the selected
T. Err(error) executes pending cleanup and returns a freshly constructed
Result::<U, E>.Err(error) from the current message with the same exact E.
The operation performs no clone, conversion, implicit error union, fault
translation, or handler invocation; ordinary Copy and move rules govern the
carrier and selected payload.
Contracts
C0-CONTRACT-001 — Clause meanings. requires { ... } declares
preconditions checked at message entry. ensures { ... } declares
postconditions checked on every normal return after the result value exists and
before ownership transfers to the caller. A non-normal Result.Err is still a
normal result value unless the contract expression distinguishes its variant.
C0-CONTRACT-002 — Result binding. In a postcondition of a non-Unit
message, result is an immutable binding of the exact declared result type.
It is unavailable in preconditions, generic requirements, bodies, and Unit
postconditions. Reading it cannot move or mutably borrow the returned value.
C0-CONTRACT-003 — Expression restrictions. Each contract block contains
zero or more Boolean expressions terminated by semicolons; the expressions are
conjoined in source order, and an empty block is true. Contract expressions
must be pure, non-allocating, non-mutating, and non-consuming.
They may read parameters, the permitted receiver view, immutable constants,
and pure messages whose contracts establish the needed result.
C0-CONTRACT-004 — Clause order and generics. Structural requires T { message signatures } clauses precede the optional precondition. The only
message clause order is generic requirements, requires { ... }, ensures { ... }, then effects { ... }.
C0-CONTRACT-005 — Verification policy. Under checked, every unproved
contract emits a deterministic runtime check. Under verified, every admitted
contract must be proved or compilation fails with proof facts. Under trusted,
the check may be omitted only while recording a named trust boundary in
provenance and reflection.
C0-CONTRACT-006 — Inheritance. An override must accept every state accepted by the inherited precondition and guarantee every inherited postcondition. It may strengthen guarantees, but cannot strengthen caller obligations or weaken base guarantees.
C0-CONTRACT-007 — Deferred snapshots. old(...), loop invariants, frame
conditions, and arbitrary heap snapshots are deferred beyond the first
selfhost-0 bootstrap. Their absence does not permit a compiler to assign them
an implementation-defined meaning.