Core-0normative target; implementation partial

ZLM1, execution engines, reflection, and deterministic behavior.

Core-0 Checked Artifacts and Execution

Status: normative target; Stage0 emits and independently validates scalar-only ZLM1 schema 1.2 and the fieldless-closed-enum extension in schema 1.3, the fieldless-closed-error extension in schema 1.4, and the bounded single-Int32-payload closed-variant extension in schema 1.5. Schema 1.6 retains fixed-width integer execution annotations through every backend. Schema 1.7 emits the bounded intrinsic Result carrier and try operation. It retains a read-only ZLM0 compatibility decoder. Schema 1.8 emits the first bounded sealed-value record, initializer, whole-local move, initialization, and explicit drop substrate through the interpreter, portable C, LLVM JIT, and LLVM AOT. Stage0 has not yet implemented general aggregate ownership, borrowing, custom destruction, defer, generic instances, or the complete package payload required below. Schema 1.9 is specified as a normative target but is not yet emitted. It binds the first runtime-rich selfhost byte kernel to catalog zerglang.selfhost-intrinsics/1; none of the 1.9 records below describe current Stage0 behavior.

Checked compilation

C0-ART-001 — Phase boundary. Conforming compilation progresses through lossless tokens, syntax, resolved declarations, typed/effect-checked semantics, an ownership/initialization CFG, drop-elaborated Core IR, and an artifact bundle. A later phase cannot reinterpret or repair an earlier phase silently.

C0-ART-002 — No unchecked execution. Only validated checked Core IR may be interpreted or materialized. A parsed, unresolved, partially typed, or ownership-unchecked tree is never executable.

C0-ART-003 — Portable semantic payload. ZLM1 is a versioned, canonical, host-pointer-free package of imports, symbols, types, effects, contracts, ownership/drop CFG, typed instructions, generic instances, and semantic identities. Indices are bounds-checked and every consumer independently validates untrusted serialized bytes.

Schema 1.3 introduces one universal type-reference namespace. The scalar sentinel denotes the intrinsic-scalar family, while the retained canonical type spelling supplies the exact scalar kind; it is not itself a universal exact scalar ID. Every other reference indexes the canonical descriptor table, whose only admitted descriptor kind in 1.3 is a closed enum. All later 1.x descriptor kinds extend this same namespace and the same function/local reference fields; they do not add parallel per-kind reference fields.

Schema 1.4 assigns descriptor kind 0 to a closed enum and kind 1 to a closed error. A canonical 1.4 payload contains at least one error descriptor; an enum-only payload remains byte-for-byte schema 1.3. Empty closed errors are valid uninhabited types, so the 1.4 invariant is about descriptor kind rather than variant count. Later 1.x record and intrinsic descriptor kinds extend the same namespace.

Schema 1.5 extends every variant record with an explicit payload count, field name, field type spelling, and universal type reference. Its current Stage0 writer admits either no payload or exactly one named Int32 payload and emits 1.5 only when at least one such payload exists. The bounded inline runtime word stores the variant tag in the low unsigned 32 bits and the exact two’s- complement Int32 payload bits in the high unsigned 32 bits. Construction, tag testing, and signed payload extraction are separate checked Core operations. Payload extraction compares the word’s low-u32 dynamic tag with the payload variant named by the operation before reading the high bits; a mismatch is a deterministic runtime fault in every execution engine. Enum-only Payload construction faults when a runtime operand is outside the signed Int32 range under exact or approximate semantics and explicitly wraps its low 32 bits under modular semantics. Enum-only and error-bearing fieldless modules remain byte-for-byte schemas 1.3 and 1.4 respectively.

Schema 1.6 assigns the previously reserved instruction word a closed scalar kind and retains the typed function/local metadata even when a module has no closed descriptors. The annotation commits the declared width and signedness used by each numeric operation and scalar store, call, and return boundary. The interpreter, portable-C backend, LLVM JIT, and LLVM AOT apply the selected numeric profile at that width: exact and approximate arithmetic fault on an out-of-range result, modular arithmetic wraps at the declared width, and division, remainder, comparison, and negation use the annotated signedness. Malformed annotations and non-canonical boundary values fail closed. Modules whose behavior needs no retained fixed-width annotation continue to emit their byte-identical canonical schema 1.2–1.5 representation.

Schema 1.7 assigns descriptor kind 2 to the compiler-provided intrinsic Result<T, E> carrier. Its descriptor identity is derived canonically from the exact nominal or scalar identities of T and E; its only variants are Ok(value: T) at tag zero and Err(error: E) at tag one. The current Stage0 writer admits only payloads representable in one 32-bit carrier word: exact scalars of at most 32 bits or fieldless enum/error values. The runtime word stores the Result tag in the low unsigned 32 bits and the payload word in the high unsigned 32 bits. The checked RESULT_TRY operation names its exact Result descriptor: tag zero validates and yields T, tag one validates E and returns a freshly packed outer Err, and any noncanonical tag or payload faults. Schema 1.7 retains schema 1.6 scalar annotations on every instruction that requires them. A schema 1.7 artifact must contain at least one canonical Result descriptor; artifacts without Result remain byte-for-byte canonical schemas 1.2–1.6.

Schema 1.8 assigns descriptor kind 3 to a bounded sealed-value record. The only admitted record has exactly one public immutable field whose type is an exact scalar type whose canonical width is at most 32 bits: Bool, Byte, Int8, Int16, Int32, UInt8, UInt16, or UInt32. The descriptor field record contains the canonical field semantic ID, UTF-8 name, public visibility, let mutability, exact scalar spelling, and the universal scalar sentinel. A descriptor with any other field count, visibility, mutability, or field type is invalid under this bounded profile. The closed field visibility and mutability tags are public zero and let zero; every other value is rejected in 1.8.

The record’s one-word runtime payload is the field’s canonical scalar word. Bool is zero or one, signed integers are canonically sign-extended, and unsigned integers and Byte are canonically zero-extended; bits outside the declared width must equal that extension. The nominal descriptor, rather than a runtime tag, distinguishes records with the same field representation. The record remains non-Copy despite containing a Copy scalar. It is admitted as a schema-1.7 Result payload through its exact low-32-bit representation. The initializer error E must independently satisfy the schema-1.7 one-word Result payload bound.

A bounded record descriptor names exactly one public initializer. Its function record has the closed callable kind initializer tag one, its declaring descriptor, canonical parameters and empty or declared effects, and exact result Result<Self, E>; ordinary algorithm messages retain callable-kind tag zero. .zli and reflection expose the descriptor, public field, initializer signature, ownership, and copy: false, but never the initializer body.

Schema 1.8 adds the checked operations VALUE_CONSTRUCT, FIELD_GET_COPY, MOVE_LOCAL, DROP_LOCAL, and DROP_ARG at closed instruction tags 30, 31, 32, 33, and 34 respectively; tags 0–29 retain their schema-1.7 meanings. VALUE_CONSTRUCT carries a descriptor reference and exact scalar annotation, consumes one scalar stack operand, and pushes a fresh initialized value of that nominal record type. FIELD_GET_COPY carries an argument/local place kind, place index, descriptor reference, field ordinal zero, and exact scalar annotation; it reads that initialized place and pushes the copied scalar without loading, copying, or consuming the record owner. MOVE_LOCAL carries a local index, requires an initialized owned local, pushes its exact value, and changes that move path to moved. DROP_LOCAL and DROP_ARG carry their local or parameter index, consume an initialized owner without a stack result, and change its path to uninitialized; they are illegal for an uninitialized or moved path. Reserved operand bits are zero and every unused scalar annotation is ZL_SCALAR_LEGACY zero.

The schema-1.8 ownership section records each owned parameter/local move path, its declaration or initialization order, and every normal, error, and control- flow cleanup successor. Paths are ordered by parameter index and then local index. State tags are uninitialized zero, initialized one, and moved two. Each cleanup edge records its source instruction, successor instruction or function exit, edge kind, and ordered drop-instruction indices; edge kinds normal, error, and control have tags zero, one, and two. Validation independently reruns the three-state ownership dataflow and requires exactly one consuming move or drop on every reachable path. Drop elaboration emits explicit cleanup edges even when destruction is runtime-trivial, in reverse initialization order. A 1.8 RESULT_TRY names an explicit error cleanup edge; that edge drops every live owner before constructing and returning the fresh outer Err. No interpreter or materializer may implement that error path as an implicit return that skips the recorded cleanup.

The first executable Stage0 writer emits normal and error cleanup edges. It reserves the canonical control-edge tag, but rejects with ZL-TYPE-0004 any bounded source whose unequal owner states at a break, continue, loop backedge, or one-sided branch join would require scope-aware control cleanup. This is a fail-closed implementation boundary, not permission to omit a required control cleanup edge from an admitted source or checked artifact.

A canonical artifact uses schema 1.8 when it contains descriptor kind 3, a schema-1.8 ownership record, or one of the schema-1.8 operations. Artifacts that need none of those features remain byte-for-byte schemas 1.2–1.7, including their prior descriptor, function, instruction, and RESULT_TRY encodings. A 1.8 reader rejects unknown record kinds, field records, callable kinds, ownership states, operation tags, references, cleanup targets, noncanonical scalar words, and missing, duplicated, or out-of-order cleanup.

This first executable profile does not admit zero- or multi-field values, non-public or mutable fields, fields wider than 32 bits, nested records, classes, borrows, custom drop, and defer. Those remain Core-0 language directions, but a Stage0 compiler implementing this profile must diagnose them before checked-module emission rather than select a host layout, erase ownership, synthesize cleanup, or fall back to a backend-specific ABI.

Schema 1.9 is the first runtime-rich selfhost extension. It admits multiple top-level declarations in one module, multiple fields and messages in one declaration, all four receiver forms, explicit effect sets, lexical loans, general aggregate ownership, and a rich Result payload. It is available only with the exact ID and content identity of zerglang.selfhost-intrinsics/1. The 1.9 writer must not emit until every interpreter and materializer implements the records and the typed invocation boundary below.

Exact schema-1.9 byte layout

Every multi-byte integer in schema 1.9 is unsigned little-endian unless a field is explicitly an opaque byte array. Records are packed with no alignment, padding, implicit terminator, or bytes between sections. A 32-byte identity is the raw SHA-256 output in digest order. NONE is 0xffffffff in an unsigned 32-bit reference. A range is start: u32, count: u32 into the named flat section; an empty range has start equal to the cumulative next entry and count zero. Every reserved field and flag bit not assigned below is zero. All multiplication/addition used to derive offsets is checked before reading. Every schema-1.9 ordering over bytes, logical preimages, IDs, or digests uses unsigned-octet lexicographic comparison with a proper prefix first. Every ordering over numeric fields uses unsigned numeric order. Host character collation, signed-byte comparison, and locale never participate.

The exact section order is:

256-byte header
string pool bytes
80-byte import records
80-byte type-instance records
u32 type-child references
80-byte declaration records
72-byte field records
64-byte variant records
176-byte function records
64-byte parameter records
64-byte local records
32-byte block records
16-byte effect-set records
u32 effect tags
32-byte owned-path records
40-byte lexical-loan records
32-byte cleanup-edge records
u32 drop-operation references
56-byte constant records
constant payload bytes
16-byte operand records
32-byte semantic-symbol-reference records
64-byte contract-operation records
32-byte typed-operation records

There is no section directory and no alignment. Section starts are derived in that order from the header counts and the two pool byte lengths. The derived end must equal module_bytes; trailing bytes are invalid. The string pool is the concatenation of each distinct nonempty canonical UTF-8 string in unsigned byte-lexicographic order, without terminators. Every string field is an offset: u32, length: u32 slice of exactly one whole pool entry. The constant pool concatenates constant payloads in constant-record order, without padding; an empty payload starts at the cumulative next byte.

The 256-byte header is:

Offset Bytes Field
0 4 ASCII ZLM1
4 2 schema major 1
6 2 schema minor 9
8 4 header bytes, exactly 256
12 4 flags, zero
16 4 numeric semantic profile
20 4 verification mode
24 32 intrinsic catalog content identity
56 32 logical module content identity
88 4 module-name string offset
92 4 module-name string length
96 4 import count
100 4 type-instance count
104 4 type-child-reference count
108 4 declaration count
112 4 field count
116 4 variant count
120 4 function count
124 4 parameter count
128 4 local count
132 4 block count
136 4 effect-set count
140 4 effect-tag count
144 4 owned-path count
148 4 lexical-loan count
152 4 cleanup-edge count
156 4 drop-operation-reference count
160 4 constant count
164 4 operand count
168 4 typed-operation count
172 4 contract-operation count
176 8 string-pool byte length, at most 0xffffffff
184 8 constant-pool byte length, at most 0xffffffff
192 8 exact total module_bytes
200 4 package-name string offset
204 4 package-name string length
208 4 semantic-symbol-reference count
212 44 reserved zeros

Fixed records use these fields in byte order; comma-separated u32 fields occupy four bytes each in the written order:

Record Exact packed fields
import, 80 bytes imported declaration nominal semantic ID [32]; module string offset, module string length, declaration string offset, declaration string length; imported module-interface digest [32]
type instance, 80 bytes type-instance ID [32]; kind, scalar kind or NONE, nominal declaration or NONE, child start, child count, flags (Copy bit zero only), reserved; reserved bytes [20]
declaration, 80 bytes declaration-nominal ID [32]; kind, visibility, flags (Copy bit zero, open bit one), name offset, name length, field start, field count, variant start, variant count, function start, function count, reserved
field, 72 bytes field ID [32]; owner kind (declaration zero, variant one), owner index, ordinal, name offset, name length, visibility, mutability, type-instance reference, flags zero, reserved zero
variant, 64 bytes variant ID [32]; declaration index, tag, name offset, name length, payload-field start, payload-field count, reserved zero, reserved zero
function, 176 bytes function-signature ID [32]; declaration index, callable kind, receiver kind, receiver type or NONE, name offset, name length, parameter start, parameter count, local start, local count, block start, block count, result type, effect-set index, owned-path start, owned-path count, loan start, loan count, cleanup-edge start, cleanup-edge count, body-operation start, body-operation count, flags zero, visibility, requires-operation start, requires-operation count, ensures-operation start, ensures-operation count; function-contract digest [32]
parameter/local, 64 bytes parameter or local ID [32]; function index, ordinal, name offset, name length, type-instance reference, flags (parameter move bit zero only; local flags zero), reserved zero, reserved zero
block, 32 bytes function index, dense function-local block ID, operation start, operation count, flags (entry bit zero only), reserved zero, reserved zero, reserved zero
effect set, 16 bytes effect-tag start, effect-tag count, reserved zero, reserved zero
owned path, 32 bytes function index, place kind (argument zero, local one, field two, temporary three), place index, parent path or NONE, type-instance reference, initialization ordinal, entry state (uninitialized zero, initialized one, moved two), reserved zero
lexical loan, 40 bytes function index, dense function-local loan ID, kind, origin owned-path index, parent loan or NONE, borrowed type-instance reference, creation operation or NONE for an entry loan, last-use operation or NONE, reserved zero, reserved zero
cleanup edge, 32 bytes function index, dense function-local edge ID, source block, successor block or NONE for exit, edge kind, drop-reference start, drop-reference count, reserved zero
constant, 56 bytes constant ID [32]; type-instance reference, reserved zero; payload offset u64, payload length u64
operand, 16 bytes kind (SSA value zero, place one, constant two, block three, contract receiver four, contract parameter five, contract result six, contract value seven), referenced index, type-instance reference or NONE for block, reserved zero
semantic-symbol reference, 32 bytes exact raw declaration, field, variant, declared-function, catalog-function, or effect-set semantic ID/digest
contract operation, 64 bytes closed tag, exact result type-instance reference, operand start, operand count, auxiliary zero, auxiliary one; exact referenced field, variant, declared-function, or catalog-function ID [32] or all zeros; flags (contract-expression-root bit zero only), reserved zero
typed operation, 32 bytes tag, result type or NONE, operand start, operand count, auxiliary zero, auxiliary one, flags zero, reserved zero

The header numeric-profile tags are exact zero, modular one, and approximate two. Its verification-mode tags are checked zero, verified one, and trusted two. Declaration/function/field visibility tags are public zero, module one, and private two. Field mutability tags are let zero and var one. Callable kinds are ordinary message zero and initializer one. All other values reject. Declaration-kind tags are value zero, class one, enum two, error three, and intrinsic four. This bounded schema-1.9 profile admits local declaration rows only for value zero, enum two, and error three. Class one rejects because this profile has no class allocation, base, or dispatch representation; the derived Class<Self> type-receiver form does not require a class declaration row. Intrinsic four also rejects: catalog intrinsics are authenticated catalog entries, never injectable synthetic local declarations. A value declaration may own ordinary fields and functions but no variants; an enum or error owns variants and functions but no ordinary fields or initializer. Every other kind/owned-range combination rejects. For callable kind zero, the function domain is the derived constant algorithm; it is not a physical field or hash part, and canonical .zli emits algorithm message. Callable kind one emits init and has no message domain. Any function in a deferred Core-0 domain rejects before schema-1.9 emission.

This schema-1.9 selfhost subset admits only sealed concrete declarations and messages. Open, abstract, override, and inheritance facts reject before emission rather than being erased; consequently every admitted declaration open flag and every function flags word is zero. A later schema must add explicit records and interface/hash facts before those Core-0 features are serialized. The declaration Copy flag is also derived: a value declaration is non-Copy, while an enum or error is Copy exactly when every field of every payload variant is structurally Copy under C0-TYPE-007 (a wholly fieldless variant set is Copy). The type-instance Copy flag is recomputed from the closed kind, catalog fact, nominal declaration flag, and child type flags; it is never an author-selected identity fact. A mismatched declaration or type Copy bit rejects before contract, load, result, or cleanup validation.

Imports are ordered by imported declaration-nominal ID and duplicates reject; each import’s module/name slices and interface digest must validate against the same imported nominal identity. Declarations are ordered by declaration-nominal ID. Variants are grouped by declaration-nominal ID. Their tags are exactly their dense semantic source ordinals beginning at zero, so physical rows are strictly ascending with no gap or duplicate. A declaration record’s field range owns exactly its ordinary fields with owner kind declaration; each variant record’s payload-field range owns exactly that variant’s payload fields with owner kind variant. Those ranges never overlap. Variant payload syntax carries no visibility or mutability modifier, so every variant-owned field derives public visibility zero and let mutability zero; any other encoded pair rejects. For each declaration in that order, its ordinary fields precede its tag-ordered variants’ payload fields; each field group uses unique contiguous semantic source ordinals beginning at zero. Functions are grouped by declaration and function-signature ID. Parameters and locals are grouped by function-signature ID; each has unique contiguous semantic ordinals beginning at zero. A parameter’s move bit is derived from its admitted type and ABI ownership: one exactly for a non-Copy, nonborrow by-value owner; zero for a Copy value and for every Ref, Mut, Slice, or allocator loan. Source syntax cannot choose it. Local flags are always zero, and any mismatched parameter/local flags reject. Blocks are grouped by function and dense block ID, and flow-operation ordinals are dense from zero within each block. Typed-operation rows put all flow operations in block order first, followed by edge-owned cleanup recipes in cleanup-edge/drop ordinal order; a block range owns only flow rows, each drop-reference range owns its cleanup-recipe rows, and the function body-operation range covers both groups exactly. Type children, effect tags, drop references, and operands are the concatenated ranges of their owning records; no item may belong to two ranges or lie outside all owning ranges. Owned paths are ordered by function and resolved logical owned-path key. Loans and cleanup edges are ordered by function and dense ID. Constants and effect sets are ordered by their logical IDs or digests. Semantic-symbol references are unique and sorted by raw 32-byte ID; every row must be referenced by at least one typed operation or owned-path field component.

The owned-path total order compares function-signature ID raw bytes, root-kind numeric value, root-identity exact logical encoding, then the field-ID sequence lexicographically; unsigned byte comparison is used and a proper prefix sorts first. A physical parent path must precede every child path. The function-body owned-path list uses this same comparator, so independent writers cannot choose different root or branch orders.

The header’s package-name and module-name slices each name one whole string-pool entry. Together they are the complete namespace input for recomputation, but the untrusted artifact does not self-authorize that namespace: both slices must be byte-equal to the validated package manifest and module-graph entry, including the canonical path identity required by C0-MOD-001. An independent decoder does not obtain the package name from an ambient path or manifest guess. Each import nominal ID is resolved against its exact provider interface, and its string slices must be byte-equal to that provider’s canonical module and declaration names. The type-instance nominal declaration word uses one combined reference namespace: import references occupy 0..import_count-1; local declaration references occupy import_count..import_count + declaration_count - 1 and subtract import_count to obtain the local declaration index. The checked sum must be strictly less than NONE. Decoding resolves either form to the referenced declaration nominal ID before type identity is recomputed. Every other record field explicitly described as a declaration index remains a local declaration index and does not use this combined namespace.

An owned-path record’s physical place encoding maps uniquely to the logical root. A runtime receiver exists only for shared, exclusive, or owned receiver kinds. For place kind argument zero, argument index zero names that runtime receiver and parameter p uses index p + 1; with receiver kind none or type, parameter p uses index p. A type receiver has no argument or owned-path slot, and any operand or path that claims one rejects. Place kind local one names the function-local ordinal. Place kind temporary three names its producing body-operation index. For place kind field two, place index is a semantic-symbol-reference index that resolves the exact field ID; its immediate logical parent/prefix must precede it physically, and resolving the chain appends that field ID to the root’s ordered field path. If any receiver, parameter, local, or temporary root’s exact type is Ref<T> or Mut<T>, the first field component performs one validated dereference to target T for field-owner matching while retaining the active entry-loan authority and shared/exclusive access mode. A shared-root path permits only observation, Copy field reads, and shared reborrow. A mutable-root path additionally permits interior mutation of the existing field owner when its type supports that operation. Field-binding move, rebind, or REPLACE_COMMIT requires mutability var; let rejects FIELD_MOVE and every binding replacement while still permitting an exact Mut-derived interior loan. Neither borrowed root permits moving or dropping the root owner. Later components match the preceding field’s target type without another implicit dereference. Roots use parent NONE; field paths never do. Any parent cycle, skipped parent, unresolved/non-field/wrong-owner symbol, or mismatched resulting type rejects, so two physical encodings cannot denote one logical path.

The initialization ordinal is derived rather than chosen. An argument root uses its logical runtime-slot ordinal; a local root uses its semantic local ordinal; a temporary root uses its producing operation’s ordinal in the function’s canonical block/operation order; and a field path uses the final field’s semantic source ordinal within its immediate owner. The validator recomputes those category-local ordinals. Runtime moves and reinitializations change the separate custody list only at their committing operation; they do not renumber these static path facts.

Entry state is also derived. A committed runtime receiver/parameter binding is initialized at function entry; its recursively addressable owner fields are initialized, while a borrow root is a live nonowning binding under its entry loan. Local and temporary roots, and their fields, start uninitialized unless an explicitly prescribed source entry initializer has already committed before the body (this bounded profile defines none). Entry-state moved two is therefore invalid in a canonical schema-1.9 record; moves during execution are validated CFG state transitions, not a forged initial state. The checker recomputes these values before cleanup validation.

Every field path reached through the implicit Ref/Mut dereference remains loan-derived and retains the exact active ancestor-loan identity and access mode. A borrow or slice operation from that path must name that loan, or a valid active child of it, as its parent; it cannot relabel the resulting P(T) as an owned origin. Parent NONE is valid only for a genuinely owned origin or the prescribed entry-loan root. Shared ancestry forbids mutation and BORROW_MUT; replacement, move, or drop through any borrowed ancestry rejects.

The operand record’s referenced index has one closed namespace per kind. SSA value zero names an exact typed-operation table row that produces a value, belongs to the same function, dominates this use, and has the carried exact type. Place one names an owned-path row in the same function. Constant two names a constant-table row. Block three names a block row in the same function and requires type NONE. Contract receiver four and contract result six require referenced index zero and the exact signature type; result remains ensures-only. A contract receiver operand exists only for a shared, exclusive, or owned runtime receiver; receiver kinds type and none reject that operand. Contract parameter five names the semantic parameter ordinal in the current function. Contract value seven names a dense prior operation ordinal in the same contract expression. Every non-block operand carries and revalidates the exact referenced type. A referenced index cannot cross its function, expression, or owning operation range, alias another namespace, or name a type-receiver runtime value.

Other operation-like physical references are also closed. An owned-path temporary producer and a loan’s creation and last-use operation are global typed-operation table indices resolving to operations in that same function; each must resolve owner kind zero in a block flow range. The producer must have the path’s exact type, and creation must not follow last use. SSA operands, normal dominance, and block operation ranges likewise name only owner-kind-zero flow rows. A parent-loan field is a preceding loan-table index in the same function. A cleanup edge’s source and optional successor are global block-table indices in the same function and resolve to the stated logical block keys; its dense edge ID remains function-local. Each drop-reference u32 is a global typed-operation index in that function naming one prescribed schema-1.9 PLACE_DROP cleanup-recipe row, and belongs to exactly one cleanup-edge range in its canonical order. A cleanup-recipe row is not in any block operation range and is executed exactly once by traversal of its owning edge, before the successor or exit handoff; it is never reached or executed as an ordinary block operation. Empty cleanup has an empty range. No recipe may occur elsewhere or belong to two edges. A recipe is owner kind one, has tag 40, P(T) as its sole operand, no result, owned-path auxiliary zero, absent auxiliary one, zero flags, and cannot produce SSA/control/loans or be named by any reference other than its exact owning drop range. REPLACE_COMMIT does not reference a separate drop row: it performs the destination’s recursive old-value drop exactly once inside its atomic commit, and its physical auxiliary one is zero. No operation, block, loan, edge, or drop reference may cross owners, use a dense ID as a table index, or be reused where unique prescribed ownership is required.

Type-instance kind tags are the catalog tags zero through nine. scalar kind is non-NONE only for kind zero; nominal declaration only for kind three; and children are empty except: Result has exact children [T, E], Ref and Mut have [T], and the catalog-closed byte/allocator instances have the children required by their catalog record. Type flags contain only the validated structural Copy bit. They are revalidated derived facts and are not identity inputs.

For a scalar type instance, the closed scalar-kind tags are Bool one, Byte two, Int8 three, Int16 four, Int32 five, Int64 six, UInt8 seven, UInt16 eight, UInt32 nine, UInt64 ten, and Index eleven. Legacy scalar tag zero is confined to prior schemas and rejects in schema 1.9; every other scalar tag rejects. A non-scalar type instance uses scalar kind NONE.

Schema-1.9 constants are admitted only for closed scalar types other than Index; nominal, owner, borrow, Unit, and target-sized constants reject. Bool, Byte, Int8, and UInt8 use one payload byte; Int16/UInt16 use two; Int32/UInt32 use four; and Int64/UInt64 use eight. Payloads are the exact little-endian unsigned bits, signed values use two’s-complement at that width, and Bool is exactly zero or one. Any other payload length or encoding rejects before its constant ID is recomputed.

Logical semantic identities

Schema 1.9 identities are hashes of logical facts, never hashes of packed records. Let F(P) be u64le(byte_length(P)) || P. Let S(E0, ..., En) be u32le(n + 1) || F(E0) || ... || F(En); S() is four zero bytes. Every tuple and list element named below uses S, including nested elements. Let H(D; P0, ..., Pn) be SHA-256 over the ASCII domain D, one zero byte, and F(P0) || ... || F(Pn). This is the domain-nul-u64le-framed-parts-v1 construction. A closed tag, flag word, or semantic ordinal is u32le. An ID or digest is its raw 32 bytes. A name is the exact accepted canonical UTF-8 identifier or dotted module identity, with no case folding or host normalization.

An optional is byte 00 for absent or byte 01 followed by the present value. The complete optional is one hash part or one S element. Empty optional, empty bytes, and S() are therefore distinct. A semantic source ordinal is fixed by checked source semantics before serialization; it is not a physical table position. Every ordered list below is encoded with S; a named tuple (A, B) means S(A, B).

A logical preimage must not contain a table index, section offset, pool offset, range, or physical record order. It also must not contain a runtime handle, context ID, allocator token, source position, host path, or target layout. The exact hash domains and ordered top-level parts are:

Fact Domain and ordered framed parts
module namespace zerglang.zlm1.module-namespace.v1; package manifest name UTF-8, dotted module identity UTF-8
declaration nominal ID zerglang.zlm1.declaration-nominal.v1; module-namespace ID, declaration-kind u32, declaration name UTF-8
type-instance ID zerglang.zlm1.type-instance.v1; optional stable catalog ID UTF-8, type-kind u32, optional scalar-kind u32, optional declaration nominal ID, ordered child type-instance-ID list
variant ID zerglang.zlm1.variant.v1; owner declaration nominal ID, semantic tag u32, name UTF-8
field ID zerglang.zlm1.field.v1; owner-kind u32, owner declaration-nominal or variant ID, semantic source ordinal u32, name UTF-8, visibility u32, mutability u32, type-instance ID, flags u32
effect-set digest zerglang.zlm1.effect-set.v1; ordered unique ascending effect-tag list
declared function-signature ID zerglang.zlm1.function.v1; owner declaration nominal ID, callable-kind u32, receiver-kind u32, optional receiver type-instance ID, name UTF-8, ordered parameter-signature list, result type-instance ID, effect-set digest
catalog function-signature ID zerglang.zlm1.catalog-function.v1; stable catalog ID UTF-8, selector ID u32, owner type-instance ID, callable-kind u32, receiver-kind u32, optional receiver type-instance ID, name UTF-8, ordered parameter-signature list, result type-instance ID, effect-set digest
parameter ID zerglang.zlm1.parameter.v1; declared function-signature ID, semantic source ordinal u32, name UTF-8, type-instance ID, flags u32
local ID zerglang.zlm1.local.v1; declared function-signature ID, semantic source ordinal u32, name UTF-8, type-instance ID, flags u32
constant ID zerglang.zlm1.constant.v1; type-instance ID, exact canonical payload bytes
function-contract digest zerglang.zlm1.function-contract.v1; declared or catalog function-signature ID, generic-requirement list, ordered typed requires-expression list, ordered typed ensures-expression list
function-body digest zerglang.zlm1.function-body.v1; declared function-signature ID, ordered local-ID list, logical block list, logical owned-path list, logical loan list, logical cleanup-edge list, logical body-operation list
declaration public-interface digest zerglang.zlm1.declaration-interface.v1; declaration nominal ID, visibility u32, declaration flags u32, public ordinary-field list, complete variant-schema list, public function-contract list
declaration definition digest zerglang.zlm1.declaration-definition.v1; declaration nominal ID, declaration public-interface digest, visibility u32, declaration flags u32, all ordinary-field list, complete variant-schema list, complete function-definition list
module interface digest zerglang.zlm1.module-interface.v1; module-namespace ID, numeric-profile u32, mandatory selected catalog content identity, direct dependency-interface list, exported declaration-interface list
module content identity zerglang.zlm1.module-content.v1; module-namespace ID, numeric-profile u32, verification-mode u32, mandatory selected catalog content identity, import list, declaration-definition list, module-interface digest
exact artifact content address zerglang.zlm1.artifact.v1; exact canonical ZLM1 bytes

A parameter-signature element is (ordinal u32, name UTF-8, type-instance ID, flags u32). The function-signature ID remains contract-free and hashes these signature facts, not parameter IDs that are derived from it. An ordinary-field-list element is the exact raw field ID. The public list is exactly the declaration’s visibility-public ordinary fields and the complete list is exactly all of its ordinary fields, each once with no omission or injection; both lists use semantic source-ordinal order, and every ID must resolve back to the matching owner and ordinal. Duplicate functions with identical logical signatures collide and reject. A catalog function is not represented by a synthetic declaration or function record: its stable catalog ID, selector ID, and complete catalog signature produce the separate catalog-function.v1 identity. A checked catalog lookup must reproduce that identity before a module may reference it.

A variant-schema element is (variant ID, ordered payload-field-ID list). Ordinary and payload fields use semantic source order; variants use tag order. A public function-contract element is (function-signature ID, visibility u32, function-contract digest), sorted by signature ID. The complete function-definition tuple is (function-signature ID, visibility, function-contract digest, function-body digest) and private functions are included. A declaration’s ordinary-field lists are ordered by semantic source ordinal; its function-definition list is ordered by signature ID.

The declaration nominal ID deliberately excludes visibility, flags, fields, variants, functions, types, contracts, and bodies. A nominal type instance is a leaf whose optional declaration part contains that nominal ID and whose child list is empty. Consequently recursive nominal references in the identity graph, including mutually recursive declaration references, can be represented and recomputed without a hash fixed point. This hash-DAG property does not admit recursive inline storage. Finite-layout validation under C0-TYPE-008 follows ordinary and variant-payload fields and rejects every direct or mutual inline owned-payload cycle in this bounded profile, because it admits no storage indirection that could break such a cycle. Non-nominal constructor children also form a directed acyclic graph; a direct or indirect type-child cycle is invalid. Result, Array<Byte>, Slice<Byte>, Ref, Mut, Unit, Never, and Allocator<BytesError> put the stable catalog ID zerglang.selfhost-intrinsics/1, not its content digest, in the optional catalog part. Scalars and nominal instances use absent there. Thus a compatible catalog clarification does not silently retag every live type.

The separate declaration public-interface digest commits the complete public schema. For BytesError, it commits all four tag-ordered variants and every ordered payload field ID, and each field ID commits its name and exact UInt64 type. Adding, removing, renaming, reordering, or retyping a payload field changes this digest but not the declaration nominal ID or nominal type-instance ID. A consumer validates both the imported nominal ID and the dependency’s exact module-interface digest; a stale pair rejects before checking the dependent module.

Direct dependency-interface elements are (dependency module-namespace ID, dependency module-interface digest) sorted by namespace ID. Export elements are (declaration nominal ID, declaration public-interface digest) sorted by nominal ID. Import elements are (imported declaration nominal ID, imported module-interface digest) sorted by imported nominal ID. Dependency digests are computed in the acyclic-module topological order required by C0-MOD-003. Each module-content declaration-definition element is (declaration nominal ID, declaration-definition digest). The list contains every local declaration exactly once and no nonlocal or extra declaration, sorted by raw declaration nominal ID under the global unsigned-octet comparator. For a manifest-public module, the exported-declaration list is exactly the local public declarations admitted by the validated public-module manifest; a private module exports the empty list. Each declaration-interface public ordinary-field and public function list contains exactly its visibility-public records, while the complete variant schema follows the declaration’s openness rules. Record visibility is revalidated against list membership. Omission, duplication, injection of a private member, or export of a nonlocal declaration rejects. The module-interface digest commits the numeric profile and the mandatory selected catalog content identity. The module-content identity commits the mandatory selected catalog content identity again and it must be the same nonzero 32 bytes carried in the schema-1.9 header. A stable catalog ID inside a type or catalog-function ID is never catalog-schema authentication. Every direct dependency interface in one checked package graph must carry the same selected catalog ID and content identity as its consumer; a mixed-catalog graph rejects even when every individual digest is otherwise authentic.

Contract expressions have an exact logical projection. A contract operand element is (kind u32, reference, exact type-instance ID). Admitted kinds are constant two with a constant ID; receiver four with receiver semantic ordinal zero; parameter five with its semantic ordinal; reserved result binding six with ordinal zero; and contract value seven with the dense ordinal of an earlier operation in the same expression. Receiver and parameter types and ordinals must exactly match the function signature. The reserved result operand is valid only in an ensures expression and has the exact declared result type, which must be structurally Copy, nonborrow, and not Unit in this bounded contract subset. No other operand kind is valid in a contract. The physical parameter, constant, and operation references are resolved to those logical facts before hashing.

Requires expressions evaluate before the body and may read their live entry receiver and parameter bindings nonconsumingly, subject to the operation rules below. Ensures expressions may name only bindings whose survival is guaranteed without an implicit snapshot: a live shared receiver, an active shared-loan parameter, a Copy nonborrow parameter, or the admitted Copy nonborrow non-Unit result. An owned or exclusive receiver, moved or non-Copy owner parameter, ended loan, type receiver, or absent receiver rejects in ensures. Schema 1.9 carries no normal-return liveness proof or hidden entry snapshot that could admit any other binding.

A contract-operation element is the list (dense expression-local operation ordinal u32, tag u32, exact result type-instance ID, ordered contract-operand list, auxiliary-zero u32, auxiliary-one u32, optional referenced semantic ID, flags u32). Tags are identity zero, field-copy one, variant-is two, pure-call three, logical-not four, numeric-negate five, bit-not six, add seven, subtract eight, multiply nine, divide ten, remainder eleven, shift-left twelve, shift-right thirteen, bit-and fourteen, bit-xor fifteen, bit-or sixteen, equal seventeen, not-equal eighteen, less-than nineteen, less-or-equal twenty, greater-than twenty-one, greater-or-equal twenty-two, logical-and twenty-three, and logical-or twenty-four. Tags two and six are reserved and reject in this bounded schema: Core-0 has no contract-expression spelling for a standalone variant test or bit-not. The validator enforces each admitted tag’s arity, operand and result types, and canonical zero auxiliaries.

A typed requires- or ensures-expression element is exactly the S list of its ordered contract-operation elements. The corresponding top-level requires/ensures part is the S list of those expression elements in semantic source order.

Contract operand order and types are closed:

Tag Exact operands and result
0 identity exactly one direct receiver, parameter, result, or constant leaf of Copy nonborrow type T; result T; valid only as the expression root
1 field-copy one live owner T, active Ref<T>, or active unsuspended Mut<T> binding whose target declares the referenced immutable field; that field’s exact type must be structurally Copy, and the result has that type
2 reserved rejected; no canonical Core-0 contract-expression spelling
3 pure-call for a shared callee, one live T, active Ref<T>, or active unsuspended Mut<T> contract binding with exact target T; none for a type receiver; then one operand per parameter in signature order; parameter and result types exactly match that signature
4 logical-not one Bool; result Bool
5 numeric-negate one signed integer scalar T; result T
6 reserved rejected; no canonical Core-0 source spelling
7–11 add/subtract/multiply/divide/remainder left then right operands of one identical numeric scalar T; result T
12–13 shift-left/shift-right integer scalar left operand T, then UInt64 shift count; result T
14–16 bit-and/bit-xor/bit-or left then right operands of one identical integer scalar T; result T
17–22 equal/not-equal/less-than/less-or-equal/greater-than/greater-or-equal left then right operands of one identical admitted scalar type; result Bool
23–24 logical-and/logical-or left then right Bool; result Bool with lazy short-circuit evaluation

No implicit widening, coercion, overloaded source lookup, reordered receiver, or omitted operand is permitted in this schema-1.9 contract subset. Every contract-produced value is Copy and nonborrow. A pure callee has an empty effect set, admits only a type receiver or a shared receiver, has no move parameter, and has only Copy nonborrow parameters and result. No-receiver callees, initializers, operator selectors, exclusive/owned receivers, mutable or consuming parameters, borrowed results, and non-Copy results reject. Tag three admits only an identifier-named ordinary message, so its canonical .name(...) spelling cannot collide with primitive operator tags. Contract checks therefore observe but never mutate, move, drop, or allocate source custody.

Field-copy references the exact field ID. Pure-call sets auxiliary zero to callee kind declared-function zero or catalog-function one, sets auxiliary one to zero, and references the exact matching function-signature ID. The callee must have an empty effect set. Every other tag has an absent referenced ID. A contract expression is one nonshared strict left-to-right postorder tree stored as a contiguous ordered list of dense operations. A contract-value operand refers only backward within that expression; every nonroot operation result is consumed exactly once in the same expression, the root is consumed zero times, and no cross-expression reference is valid. Exactly the final operation has the contract-expression-root bit, every earlier flags word is zero, and the root has exact Bool type. Identity tag zero is valid only for that final root and its operand must be one direct leaf binding or constant, never contract value kind seven. A nonroot identity, identity chain, or identity wrapper around a compound expression rejects as a noncanonical spelling of the same tree.

Evaluating a tag-three shared call creates a synchronous shared child entry loan from the exact current-frame contract binding. A Ref<T> or Mut<T> binding must resolve an active current-frame loan with target T; a live owned T binding may be borrowed only in requires, or in ensures when that binding is in the survival set above. The child is installed for the pure callee and ended on normal return or fault before contract evaluation continues; its parent or owned origin remains live, and Mut or owner access is suspended for the entire child extent. A table token, inactive loan, or ancestor-frame loan that skips the immediate contract-evaluator frame never authorizes the call. This transition is intrinsic to typed contract evaluation and requires no body BORROW_SHARED operation. Field-copy through Mut<T> is likewise a single shared observation under that exact unsuspended loan; it neither erases nor splits exclusive provenance.

Operations are lazy typed expression definitions, not an eager postfix program. Logical-and and logical-or evaluate with Core-0 short-circuit semantics, so a skipped right subtree neither executes nor faults. Requires expressions and then ensures expressions evaluate left-to-right in semantic source order and stop at the first false clause. Absent and explicit empty contract clauses normalize to the empty list; their physical range is cumulative-next start with count zero, and canonical .zli omits an empty clause. Schema 1.9 admits no generic requirements, so its encoded generic-requirement list is exactly empty. These rules make canonical typed contract expressions sufficient to independently reconstruct and validate the complete canonical public interface; canonical .zli is regenerated from this typed representation rather than trusted source text.

The versioned schema-1.9 contract printer is zerglang.zli.contract-printer/1. It recursively prints the validated typed tree, not physical postfix order. Receiver, parameter, and result bindings print as self, their exact declared parameter name, and result. Bool constants print false or true. Contract integer constants exclude Byte and Index; the admitted exact types use the mandatory suffixes i8, i16, i32, i64, u8, u16, u32, or u64. They print the shortest exact base-ten magnitude followed immediately by that suffix, with - before a negative signed magnitude, no plus sign, and no leading zero except the single digit 0. Lexical unary minus applied directly to an integer literal is canonically folded into one signed constant, including the signed minimum; tag five with a constant operand rejects. Tag five is reserved for negating a nonliteral typed subtree, so the printer/parser normalization has only one tree for a negative literal. Identity prints its direct leaf operand in parentheses. Field-copy prints (<operand>.<exact field name>). A shared pure-call prints (<receiver>.<exact message name>(<arguments>)); a type pure-call prints (<canonical owner type>.<exact message name>(<arguments>)). Arguments are comma-plus-one-ASCII-space separated, and an empty argument list is (). Every unary operation prints (!<operand>) or (-<operand>). Every binary operation prints (<left> <operator> <right>), with the exact Core-0 spellings + - * / % << >> & ^ | == != < <= > >= && || and one ASCII space on each side. Tags two and six have no print form and reject.

The interface printer appends each nonempty clause to the signature as exactly requires { E0; E1; } or ensures { E0; E1; }, preserving clause source order, using one ASCII space at every shown boundary, no internal newline, and one semicolon per expression. Empty clauses are omitted. Names and owner type spellings come from the validated same/direct-dependency interface or selected catalog and must be uniquely source-resolvable; otherwise an exported contract rejects. The surrounding canonical declaration printer retains its specified UTF-8 and LF bytes. Thus two independent printers have an exact byte algorithm, not merely an equivalent semantic tree.

Every field, variant, or declared-function ID referenced by an exported/public contract must resolve to a public member present in the same module interface or an exact direct-dependency provider interface. A catalog-function reference must resolve under the selected catalog ID and content identity. Unresolved, private-only contract references reject, as do transitive-only, stale, unimported, or declared-versus-catalog-kind-confused references. Private contracts may reference admitted private facts because they are excluded from .zli but remain committed by declaration-definition and module-content identities.

Effect-set records, blocks, owned paths, lexical loans, cleanup edges, operands, contract operations, and typed operations do not carry standalone semantic IDs. The function-body projection uses the following exact S elements and keys:

  • a block key is (function-signature ID, dense function-local block ID). A body-operation key is (function-signature ID, owner kind u32, owner key, semantic operation ordinal): owner kind zero carries a block key for a normal flow operation and owner kind one carries a cleanup-edge key for an edge-owned drop recipe;
  • a block element is the list (block key, entry flag u32, ordered flow-body-operation-key list); exactly one block has entry flag one;
  • an owned-path key is (function-signature ID, root kind u32, root identity, ordered field-ID path). Root kinds are receiver zero, parameter one, local two, and temporary three. Their root identities are respectively receiver ordinal zero, parameter ID, local ID, and producing body-operation key;
  • an owned-path element is the list (owned-path key, optional parent owned-path key, exact type-instance ID, initialization ordinal u32, entry state u32), where entry states are uninitialized zero, initialized one, and moved two;
  • a loan key is (function-signature ID, dense creation-order loan ID) and a loan element is the list (loan key, loan kind u32, origin owned-path key, optional parent-loan key, borrowed type-instance ID, optional creation-operation key, optional last-use-operation key);
  • a cleanup-edge key is (function-signature ID, dense edge ID) and a cleanup-edge element is the list (cleanup-edge key, source block key, optional successor block key, edge kind u32, ordered cleanup-recipe operation-key list); absent successor is the exit marker;
  • a logical body operand is (kind u32, resolved reference, optional exact type-instance ID). SSA value, place, and constant operands resolve to an operation key, owned-path key, or constant ID and carry the present exact type; a block operand resolves to a block key and carries absent type; and
  • a body-operation element is the list (body-operation key, tag u32, optional result type-instance ID, ordered logical-operand list, logical auxiliary zero, logical auxiliary one, flags u32).

A logical auxiliary is (kind u32, payload). Kinds are absent zero, literal u32 one, type-instance ID two, declaration nominal ID three, field ID four, declared function-signature ID five, catalog function-signature ID six, effect-set digest seven, loan key eight, owned-path key nine, cleanup-edge key ten, body-operation key eleven, block key twelve, and variant ID thirteen. Absent has empty payload; all other payloads have the exact representation named. Each typed-operation tag fixes both auxiliary kinds. Thus an INTRINSIC_CALL logical projection uses the resolved catalog-function ID, never a raw selector or catalog-table index. Lists retain CFG semantic order: locals by ordinal, blocks by dense ID, owned paths by owned-path key, loans by dense ID, cleanup edges by dense ID, and body operations as all flow operations by block ID/operation ordinal followed by all edge-owned cleanup recipes by edge ID/drop ordinal.

Block IDs are derived by deterministic depth-first preorder of the normalized reachable CFG, with entry block zero. Successors are visited in semantic arm order before any numeric ID exists: straight fallthrough; conditional true fallthrough then false target; source-ordered match arms; loop body then loop exit; and source-ordered synthetic blocks. A previously visited successor is not renumbered, and unreachable blocks reject. Cleanup edges use one exact list algorithm: scan source blocks by dense ID; within each source first append try-error edges by ascending owning flow-operation ordinal, then append that block’s terminal successor or exit edges in the semantic arm order above. Dense edge IDs are the indices in that single list. The edge kind is derived, not chosen: return for a function-exit RETURN, try-error for the unique edge reverse-bound from a RESULT_TRY, break/continue/backedge for the corresponding structured source transfer, join for an explicit synthesized state-reconciliation transfer into a multi-predecessor join, branch for a remaining conditional arm, and fallthrough for the remaining straight successor. Those cases are tested in the listed priority and are mutually exclusive. An encoded dense ID, kind, source, or successor that disagrees with this reconstruction rejects.

Tags zero through fifty-two have this exact logical projection. V(T) is an SSA value operand of exact type T, P(T) a place operand of exact type T, C(T) a constant operand of exact type T, and B a block operand. -- means absent auxiliary and no result means the result-type optional is absent:

Tag Ordered operands and result Logical auxiliary zero; one
0 CONST C(T); result T --; --
1 NEG V(T); result T --; --
2–5 ADD/SUB/MUL/DIV V(T), V(T); result T --; --
6–7 EQ/LT V(T), V(T); result Bool --; --
8 LOAD_LOCAL argument-or-local root P(T); result T owned-path key; --
9 STORE_LOCAL destination local-root P(T), value V(T); no result owned-path key; --
10 CALL active-loan P/V(Ref<Self>/Mut<Self>) or moved-owner V(Self) runtime receiver for shared/exclusive/owned, none for type/none, then exact V copy/owned or active-loan P/V arguments in signature order; exact declared result declared function-signature ID; effect-set digest
11 JUMP target B; no result block key; --
12 JUMP_IF_FALSE condition V(Bool), false target B; no result; true target is the next dense block block key; --
13 ASSERT_TRUE V(Bool); no result --; --
14 ASSERT_EQ V(T), V(T); no result --; --
15 RETURN V(T) of the function’s exact result type; no operation result --; --
16 REM V(T), V(T); result T --; --
17–20 NE/LE/GT/GE V(T), V(T); result Bool --; --
21–23 BIT_AND/BIT_OR/BIT_XOR V(T), V(T); result T --; --
24 NOT_BOOL V(Bool); result Bool --; --
25 ENUM_CONST none; exact owner result variant ID; --
26 ENUM_IS_VARIANT rich owner P(T) or active-loan P/V(Ref<T>/Mut<T>); nonconsuming result Bool variant ID; --
27 ENUM_CONSTRUCT_I32 exact payload V(T); exact owner result variant ID; field ID
28 ENUM_PAYLOAD_I32 exact owner V(T); exact field result variant ID; field ID
29 RESULT_TRY carrier V(Result<T,E>); result T exact inner carrier type-instance ID; error cleanup-edge key
30 VALUE_CONSTRUCT one bounded field V(T); exact nominal result declaration nominal ID; field ID
31 FIELD_GET_COPY owner P(T); exact Copy field result field ID; --
32 MOVE_LOCAL local P(T); result T owned-path key; --
33–34 DROP_LOCAL/DROP_ARG owner P(T); no result owned-path key; --
35 UNIT_VALUE none; result Unit --; --
36 AGGREGATE_CONSTRUCT one value per field in declaration order; exact nominal result declaration nominal ID; literal field count
37–38 FIELD_COPY/FIELD_MOVE owner P(T); exact field result field ID; --
39 PLACE_MOVE P(T); result T owned-path key; --
40 PLACE_DROP P(T); no result owned-path key; --
41 BORROW_SHARED genuinely owned origin P(T) with parent NONE; loan-derived P(T) retaining and naming its exact active Ref<A>/Mut<A> ancestor whose validated dereference-and-field path yields T; direct whole-target parent loan P/V(Ref<T>) or P/V(Mut<T>); or active P/V(Slice<Byte>) when T is Slice<Byte>; exact Ref<T> result loan key; --
42 BORROW_MUT genuinely exclusive owned origin P(T) with parent NONE; loan-derived P(T) retaining and naming its exact active Mut<A> ancestor whose validated dereference-and-field path yields T; or direct whole-target parent loan P/V(Mut<T>); exact Mut<T> result loan key; --
43 BORROW_SLICE_BYTE receiver P(Array<Byte>), active-loan P/V(Ref<Array<Byte>>/Mut<Array<Byte>>), or the exact active-loan P/V(Ref<Bytes>/Mut<Bytes>) SDK-facade form, plus V(UInt64) start/end; result Slice<Byte> loan key; catalog Array<Byte>.slice function-signature ID
44–45 RESULT_OK_RICH/RESULT_ERR_RICH exact V(T) or V(E) payload; exact carrier result carrier type-instance ID; literal tag zero or one
46 RESULT_TRY_RICH exact V(Result<T,E>) carrier; exact Ok payload result outer carrier type-instance ID; error cleanup-edge key
47 INTRINSIC_CALL active-loan P/V(Ref<Self>/Mut<Self>) or moved-owner V(Self) runtime receiver for shared/exclusive/owned, none for type/none, then exact V copy/owned or active-loan P/V catalog arguments; exact catalog result catalog function-signature ID; effect-set digest
48 REPLACE_COMMIT destination P(T), initialized replacement V(T); no result destination owned-path key; --
49–50 SHIFT_LEFT/SHIFT_RIGHT integer V(T), V(UInt64) shift count; result T --; --
51 VARIANT_CONSTRUCT one initialized V(T) per payload field in semantic ordinal order; exact enum/error owner result variant ID; literal payload-field count
52 BYTE_BUILDER_FINISH one exact initialized P(BytesBuilder) owner; result exact Bytes --; --

For tags 1–7, 14, 16–24, and 49–50, T, arity, signedness, and result obey the already retained schema-1.6–1.8 scalar annotations and validation rules. Every named signature, field, variant, path, block, loan, cleanup edge, type, and effect must resolve in the same checked logical closure. The physical auxiliary words hold the corresponding canonical table reference or literal; the logical projection above always substitutes the resolved ID, digest, or key before hashing. Any operand count, order, result optional, auxiliary kind, or physical-to-logical resolution not listed here rejects.

Schema 1.9 uses one disjoint canonical operation family. Tags 27 and 28 and tags 30 through 34 are noncanonical in a 1.9 body; their unchanged bounded meanings remain valid only in prior schemas. A 1.9 writer uses VARIANT_CONSTRUCT for every payload variant, AGGREGATE_CONSTRUCT for ordinary record construction, FIELD_COPY/FIELD_MOVE for ordinary or payload fields, and PLACE_MOVE/PLACE_DROP for ownership paths. Fieldless variants continue to use tag 25. In schema 1.9 tag 26 is a nonconsuming place/active-loan tag test so its true-edge refinement binds the same owner path; its legacy value-operand meaning remains only in prior schemas. Tag 29 RESULT_TRY admits only the exact schema-1.7 one-word carrier shape; tag 46 RESULT_TRY_RICH admits only a rich carrier, and the two shapes never overlap. UNIT_VALUE tag 35 is the only encoding of catalog selector zero; INTRINSIC_CALL rejects selector zero. BORROW_SLICE_BYTE tag 43 is the only encoding of catalog selector six and requires its matching caller-local byte slice loan; INTRINSIC_CALL rejects selector six, and ordinary CALL rejects the exact declared Bytes.slice facade signature. For tag 43, exactly one byte-slice loan record names the receiver owned path as origin, this operation as creation, its exact reachable last use, and Slice<Byte> as borrowed type. When the tag-43 receiver is a Ref/Mut loan view, the new slice loan names that parent loan and reuses its exact underlying owner path as origin. Before resolving a pointer, bounds, or new loan, tag 43 nonmutatingly checks the exact canonical preconditions start <= end and end <= current_initialized_length of that underlying byte array. This check also applies when a source Bytes.slice call is fused directly to tag 43. A false precondition is the ordinary contract/program fault and creates no loan, pointer, bounds, custody, or state change. That direct length read is the complete specialized evaluation of the catalog selector-six and Bytes.slice requires contract. It creates no separate contract tag-three operation, length-call frame, or child loan, so hypothetical call-depth/resource exhaustion for that elided call cannot change the result. The exact decision order is: validate operand types and byte-kernel/loan provenance; perform the nonmutating bounds/precondition check; on false, program-fault unchanged; only on true, preflight tag 43’s bounded-loan and publication metadata; then atomically commit the loan and its bounds. A metadata failure after a true check changes no loan or state. No ordinary call result, return, store, carrier, or capture may manufacture or transport that slice value.

The exact sdk.bytes.Bytes.slice definition is a certified forwarding-body exception, not an ordinarily callable Slice-returning body. Its sole canonical shape is: the shared receiver entry loan; the private ordinal-zero storage: Array<Byte> field path derived through that loan; the two UInt64 parameter loads; one tag-43 operation over that field path; and an immediate tag-15 ephemeral return of that same loan value. No other operation, local, store, carrier, capture, cleanup omission, or returned value is admitted. The body is checked and hashed as the facade definition, but a source call to its exact signature is lowered in the caller directly to tag 43, never tag 10. In that caller form the active Ref<Bytes> (or valid more-exclusive reborrow) is accepted only under the selected catalog-bound sdk.bytes interface and private byte-kernel object provenance; the engine resolves the same private storage owner and preserves the caller’s exact loan and bounds. Tag 15’s Slice transport is valid only as the immediate final operation of this one certified body and hands the owner and bounds directly to the caller-local loan at the atomic call commit. A fault ends the child loan without publication. This exception never creates a typed-buffer slot or an ordinary inter-frame Slice result.

VARIANT_CONSTRUCT physical auxiliary zero is a semantic-symbol-reference index resolving the exact variant ID and auxiliary one is its exact payload field count. The result is the nominal owner type, and every operand exactly matches the corresponding payload field type. All operand values are produced left-to-right; construction initializes private scratch fields in ordinal order and publishes only the complete variant. A fault or resource failure drops only initialized scratch fields in reverse order and publishes no owner. Zero-payload use rejects because tag 25 is canonical for that shape.

For a variant-owned FIELD_COPY or FIELD_MOVE, validation must prove the owner currently has that exact active variant. Construction establishes the fact. Tag 26 followed directly by JUMP_IF_FALSE establishes it only on the true fallthrough branch for that exact owned path or loan’s underlying origin; replacement or owner move kills it, and joins retain only facts true on every predecessor. The decoder reruns this dataflow. FIELD_MOVE changes the exact payload-field move path to moved, so later access rejects and cleanup skips it while dropping remaining initialized payload fields in reverse order. A borrowed refinement permits only Copy field observation through shared access and never FIELD_MOVE; an inactive, unknown, stale, or wrong-variant payload access rejects.

BYTE_BUILDER_FINISH is admitted only in the exact catalog-bound sdk.bytes.BytesBuilder.finish definition. Its operand is the initialized owned-self path, has no active loan overlapping that owner, and consumes that path while transferring the same live token to the exact Bytes result. At one atomic commit it changes both the public type-instance ID and private intrinsic kind, preserving initialized bytes, length, capacity accounting, allocator/provider provenance, and private origin. It performs no allocation, copy, deallocation, handle creation, byte-account change, or provider consultation. Result/metadata preflight occurs before commit; any pre-commit failure leaves the Builder path initialized and owned, while success leaves it moved and only the returned Bytes may drop the token. Both physical auxiliaries are zero. No aggregate construction, replacement, declared call, or other type pair may substitute for this op. At commit the existing Builder custody-list entry is retagged in place; it is not removed, reappended, or reordered relative to other live owners.

Tag 8 LOAD_LOCAL admits only an argument or local root of structurally Copy nonborrow type; it never reads a field, temporary, owner, or borrow. Moving an owner uses PLACE_MOVE, and field reads use tag 37. Tag 9 STORE_LOCAL names only a local root. It may initialize an uninitialized destination with an exact value, consuming that value when it is non-Copy; it cannot store into an argument, field, or temporary. Overwriting an already initialized destination is canonical only for a structurally Copy nonborrow value; initialized owner replacement uses REPLACE_COMMIT so the old owner remains live until the replacement commits.

Whenever one operation carries the same logical entity through an operand and an auxiliary, both resolutions must be exactly equal. This includes jump block operands and block auxiliaries; load/store/move/drop place operands and owned-path auxiliaries; replacement destinations; carrier operands and carrier type auxiliaries; and call signatures and effect-set auxiliaries. A borrow’s loan record must name that operation, its exact origin place operand, and its exact result borrowed type. A RESULT_TRY cleanup auxiliary must resolve to the unique try-error edge whose source block contains that owning RESULT_TRY operation; each such edge is reverse-bound to exactly one owning try and no other operation. A mismatched redundant reference rejects before hashing or execution; no consumer may choose one copy over the other.

For typed-operation auxiliaries whose logical kind is declaration, field, variant, declared function, catalog function, or effect set, the physical word is a semantic-symbol-reference-table index. The operation tag fixes the expected symbol kind. The decoder resolves the raw 32-byte symbol against an admitted local record, an exact public member in a direct-dependency interface, or the selected catalog; unresolved, private imported, transitive-only, wrong-kind, or ambiguous matches reject. In particular, tag 10 CALL uses a declared-function symbol then an effect-set symbol, so local and direct-import calls share one physical encoding. Tag 47 uses a catalog-function symbol then an effect-set symbol. Identity-like auxiliaries never overload a local table index or raw catalog selector.

The physical contract-operation table is grouped by function-signature ID, requires before ensures, expression source order, then dense operation order; each root bit ends one expression. The one shared operand table is allocated by function-signature order, then requires expressions, ensures expressions, then body operations, and by operation order within each group. Every operand belongs to exactly one operation range.

Identity construction proceeds in strict dependency waves: package and module namespaces; declaration nominal IDs; type instances and effect sets; constants; variants; fields; function signatures; parameters and locals; contracts; declaration interfaces; module interfaces in dependency-graph topological order; bodies and declaration definitions; then module content identity is computed last. A catalog-function ID is available after its constituent type/effect identities and catalog entry are validated. This order prevents declarations, fields, functions, parameters, or types from hashing an ID derived downstream from themselves.

Only after logical identities exist does the writer sort tables, assign indices, concatenate pools, and fill offsets and ranges. Type-instance leaf depth is zero; nonleaf depth is one plus maximum child depth. Same-depth type instances are ordered by logical preimage bytes, then by recomputed type-instance ID, before physical child or nominal indices are materialized. Permuting an in-memory logical collection before canonical emission preserves every logical identity and produces byte-identical canonical ZLM1. Directly permuting serialized records, even while consistently rewriting references, is rejected as noncanonical.

Every non-root 1.9 record and pool entry must be owned and reachable exactly as prescribed; no unreferenced physical record or pool entry is canonical. Every field, variant, function, parameter, local, block, path, loan, cleanup edge, and contract operation belongs to exactly one owner range. Every typed body operation belongs to exactly one block flow range or one cleanup-edge recipe range, never both. Every operand, type-child, effect-tag, and drop-reference element belongs to exactly one range. Every semantic-symbol reference is used and resolves with the operation- or path-required kind. Every type is reachable from a retained declaration, signature, contract, body, constant, or another reachable type; every effect set and constant is referenced; and every string-pool entry is referenced. Every non-Copy owned runtime receiver, parameter, local, or owner-producing typed-operation result has exactly one corresponding root/temporary owned-path record, and every addressable or partially moved owner field has exactly its canonical parent-linked field path. Every loan origin resolves one prescribed path. Omitting or duplicating any such path rejects before execution; a Copy/borrow-only value has no path except where an operand or entry-loan rule above explicitly prescribes one. Imports and declarations are module-content roots. Orphan rows, duplicate ownership, and injected unused strings, types, constants, or effects reject even when their local IDs and ranges are otherwise valid.

A decoder resolves every physical reference, reconstructs these logical projections, recomputes every carried ID and digest, rejects a duplicate or mismatch, and separately rejects noncanonical physical order and reachability. The logical module-content identity is distinct from the exact artifact content address. The artifact address is H(zerglang.zlm1.artifact.v1; exact canonical ZLM1 bytes) and is never embedded in those bytes or the logical module-content preimage. A schema-layout-only change can therefore alter the artifact address without changing logical semantics. Machine-readable independent golden vectors, including exact parts, framed preimages, and digests, are schema-1.9-semantic-identities-v1.json.

A contract-bearing schema-1.9 module is exactly one with at least one nonempty requires or ensures expression range. It uses verification mode checked and evaluates the canonical typed contract checks. A verified or trusted contract-bearing schema-1.9 module is rejected because this layout carries no proof or trust-provenance section. This is a fail-closed pre-fixed-point staging boundary: it does not weaken BOOT-PROFILE-006, which requires all three policies for the fixed point. A later evidence-bound schema extension is required before contract-bearing schema-1.9 compiler source can satisfy that profile.

The 1.9 typed-operation auxiliaries are closed. UNIT_VALUE has no operands and both auxiliaries zero. AGGREGATE_CONSTRUCT consumes fields in declaration order and writes declaration-symbol-reference index/field count. FIELD_COPY and FIELD_MOVE take one owner operand and write field-symbol-reference index/zero. PLACE_MOVE and PLACE_DROP take one place operand and write owned-path index/zero. BORROW_SHARED and BORROW_MUT take one place and write loan index/zero. BORROW_SLICE_BYTE takes receiver place, UInt64 start, and UInt64 end, then writes loan index and the catalog slice-function symbol-reference index. RESULT_OK_RICH and RESULT_ERR_RICH take one payload and write carrier type-instance index and tag zero or one. RESULT_TRY_RICH takes one carrier and writes outer carrier type-instance and error cleanup-edge index. INTRINSIC_CALL takes a runtime receiver only for shared, exclusive, or owned receiver kinds, then arguments in signature order, and writes catalog-function and effect-set semantic-symbol-reference indices. Type and none receivers contribute no operand. REPLACE_COMMIT takes destination place then initialized replacement and writes destination owned-path index and zero. VARIANT_CONSTRUCT takes payloads in field order and writes the variant-symbol-reference index and exact payload count. BYTE_BUILDER_FINISH takes the initialized owned-self Builder place and writes both auxiliaries zero. Any unused result, operand range, auxiliary, or flag is the exact zero/NONE value prescribed above.

A 1.9 module header adds the catalog content identity and counts for the import, declaration, field, variant, function, parameter, local, block, type-instance, effect-set, owned-path, operand, lexical-loan, complete cleanup edge, constant, semantic-symbol-reference, contract-operation, and typed-operation tables. Every count is unsigned 32-bit and every pool byte-length is unsigned 64-bit with checked conversion to host storage. Records use the exact canonical orders above. Duplicate logical IDs, integer overflow, a reserved nonzero word, an orphan record, or a reference outside its declared table is noncanonical.

The declaration record contains its 32-byte declaration-nominal ID, closed admitted kind (value zero, enum two, or error three), visibility, copy bit, UTF-8 name, and half-open field, variant, and function ranges. Reserved class one and intrinsic four reject in this bounded profile as specified above. The module namespace comes from the validated header rather than this record. Fields are in source declaration order and contain their 32-byte field ID, declaring declaration, UTF-8 name, visibility, mutability, exact type-instance reference, and initialization ordinal. This represents multiple declarations and multiple fields without selecting a host layout. Declaration and field identities are validated independently of table order.

The canonical type-instance table is unique and child-before-parent. Within the same dependency depth, records are ordered by logical preimage bytes and then recomputed type-instance ID before physical references are materialized. Each record contains a closed kind, a scalar-kind or nominal declaration reference when applicable, an ordered child-reference list, and a recomputed 32-byte type-instance ID. Kind tags are scalar zero, Unit one, Never two, nominal three, Result four, Array<Byte> five, Slice<Byte> six, Ref seven, Mut eight, and Allocator<BytesError> nine. Ref and Mut may appear only as shared/exclusive receiver types, loan-admitted parameter types, or transient loan-producing/consuming SSA/operand types tied to one exact active loan. This bounded schema forbids Ref and Mut locals. It admits kind-nine Allocator<BytesError> only as the sole child of exact Ref<Allocator<BytesError>>. That Ref may appear only as a function parameter, its full-extent entry loan, or a synchronous immediate-caller reborrow/call operand. Direct owned Allocator values and every allocator receiver, field, local, capture, carrier, result, or Mut<Allocator<BytesError>> reject. No other kind-nine parent or use is canonical. It admits one Slice<Byte> local form only: a single-initialization transient caller-local bound directly to one tag-43/facade-call loan, with the same loan ID, owner, bounds, and last use; it cannot be copied, reassigned, or have a second binding. A local place therefore cannot launder or ambiguously alias loan provenance. These loan types cannot inhabit stored fields, variants, carriers, captures, or function results. Slice may also name the declared result of the catalog Array<Byte>.slice selector and its exact Bytes.slice SDK facade. This is the sole compiler-known declared-result exception and validates as a transient caller-local loan rather than a storable result. None may appear in a stored field, variant, rich carrier, or capture, and no source-defined message or other selector may return Slice.

Each function record carries its function-signature ID, visibility, canonical typed requires/ensures ranges, and recomputed function-contract digest in addition to callable kind and declaration. Receiver-kind tags are none zero, shared Ref<Self> one, exclusive Mut<Self> two, owned Self three, and type Class<Self> four. none is valid only for an initializer. The receiver type, every parameter/local type, and result name one type-instance record. A type receiver may name a value descriptor for a catalog-known construction selector; it does not allocate a class instance.

An initializer’s name slice and function-signature name hash part are exactly UTF-8 init; empty or alternative names reject. An admitted ordinary message name is exactly one canonical identifier selector. This bounded layout has no operator-selector token/arity field, so operator-message declarations and direct operator-message calls reject before schema-1.9 emission; the closed scalar operation tags remain available for primitive operator lowering.

Receiver encoding is exact: none uses absent receiver type; shared and exclusive use exact Ref<Self> and Mut<Self> type instances; owned uses the owner Self type instance; and a type receiver stores the owner Self type-instance ID because Class<Self> is a derived compile-time receiver form, not a type-instance constructor. A type receiver is compile-time-only and contributes no typed-buffer v1 slot. Any other receiver-kind/type pairing rejects.

Every function names one canonical effect-set record. That record is an unsigned 32-bit count followed by unique ascending tags: io zero, alloc one, time two, random three, reflect four, unsafe five, and abort six. An empty effect set is a zero count, not an absent record. Unknown, duplicate, or unsorted tags are invalid, and a call’s set must be a subset of its caller’s set. The alloc tag never substitutes for an explicit allocator capability.

A lexical-loan record contains a function-local loan ID, kind (shared zero, exclusive one, byte-slice two), exact origin place, optional parent-loan ID, creation operation, last reachable use, and borrowed type-instance. Entry loans are listed first in runtime argument order. Each shared/exclusive receiver or Ref/Mut parameter has exactly one entry loan whose origin is that canonical receiver/parameter argument-root owned path, whose creation is NONE, whose parent is NONE, and whose borrowed type is the exact signature loan value type Ref<T> or Mut<T>. The origin path is checked separately as the underlying target owner T, and the loan kind must match the wrapper. Every internal Slice<Byte> parameter similarly has one kind-two entry loan rooted at that parameter, with creation and parent NONE and borrowed type exact Slice<Byte>; the external typed-buffer boundary still rejects such a slot. Every entry loan’s last-use field is NONE, meaning the conservative full callee extent through requires, body, ensures, and normal or abrupt teardown, even when the binding is unused. An outermost host loan is admitted by the driver. A nested entry loan must match a reborrow created by the immediate caller frame; a table token or ancestor-frame loan alone is insufficient.

Body-created loan IDs follow entry loans in dense creation order. Their creation and unique nonempty last use are global same-function typed-operation indices. The last-use operation is itself a use, is reachable after creation, and postdominates every reachable use of that loan. A body whose branch- incomparable uses have no unique such final operation rejects before schema-1.9 emission; NONE never gives a body-created loan full-frame extent. Reborrowing an entry or body loan names that loan as parent. Any child reborrow of an exclusive parent, including shared Mut<T> to Ref<T>, suspends that parent. It is restored only after the final overlapping shared child or exclusive child ends; sequential siblings and normal/fault teardown use the same rule. A call’s shared/exclusive receiver and every Ref, Mut, Slice, or allocator-loan argument may be a P entry-loan binding or a V body-reborrow result only when it resolves to one exact active current-frame loan of the required type and mode. The exact single-initialization transient Slice local above is also a P binding of its one tag-43 loan; no other borrow local is admitted. The call operation creates the immediate child entry reborrow for the callee; it applies the same suspension rule through return and restores the parent only if it is still live and no overlapping child remains. An active Slice<Byte> loan may also create the exact synchronous shared Ref<Slice<Byte>> child required by catalog selectors nine and ten; that child retains the same owner, bounds, and parent identity, and an unbounded owner token is never sufficient. Thus forwarding a Slice or allocator loan is representable, while mere table membership, an inactive loan, or an ancestor-frame token rejects. Copy arguments load through tag 8, owned arguments move through PLACE_MOVE, and type/none receivers contribute no operand. A body-created byte-slice loan must have a non-NONE tag-43 creation; an entry Slice loan is the explicit creation-NONE exception. Loan IDs are otherwise dense in creation order. A byte-slice’s dynamic half-open bounds remain typed operation operands rather than serialized addresses. Validation reruns loan liveness: many shared or one exclusive overlapping loan is legal; move, replacement, mutation, or drop conflicts with every incompatible live loan; and a loan is live at a join when live on any predecessor.

Before CALL or INTRINSIC_CALL changes state, the validator/runtime checks the complete receiver and argument matrix, exact types and modes, aggregate alias conflicts, active immediate-frame loan provenance, all child-frame/loan and result-metadata resources, and every owned transfer. Only after all checks succeed does one atomic commit install child entry loans and owned slots in logical runtime-slot order and suspend their parents. Any precommit failure leaves caller custody and every parent loan unchanged; a postcommit callee fault unwinds the child frame and restores only parents still entitled under the rules above.

Each CFG edge has exactly one complete cleanup edge record containing a dense edge ID, source block, successor block or exit sentinel, closed edge kind, and an ordered list of typed drop-operation indices. Edge-kind tags are fallthrough zero, branch one, join two, return three, try error four, break five, continue six, and loop backedge seven. Cleanup is reverse initialization order recursively through initialized fields. A path-specific drop reconciles unequal owner state before a join. Missing, duplicated, or engine-inferred cleanup is invalid even for a runtime-trivial value. Ownership dataflow includes the exact ordered current-frame custody sequence, not only the set of initialized paths. After predecessor-edge recipes, every predecessor of a join or backedge must present the identical live custody sequence; equal live sets in different acquisition orders reject before schema-1.9 emission. A cleanup edge’s recipe list is the reverse-order restriction of its unique incoming custody sequence to the exact paths that must die on that edge, after removing any non-addressable protected result or error payload. Thus one hashed recipe list cannot stand for two dynamic drop orders. Traversing an edge executes its edge-owned PLACE_DROP recipes once in listed order, then performs the successor/exit handoff; those rows never execute in a block. For RESULT_TRY and RESULT_TRY_RICH, the operand is exactly Result<T,E> and the enclosing function result is exactly Result<U,E> with the same E. Tag 29’s auxiliary zero retains its exact prescribed legacy inner-carrier identity; tag 46’s auxiliary zero resolves the exact outer type. Auxiliary one resolves one kind-four edge whose source is the containing block, whose successor is NONE, and which is reverse-bound to this operation only. The operation first reads and validates the canonical zero/one carrier tag without changing state; an invalid tag program-faults with the input untouched. On Ok, it preflights only the exact T SSA binding and, when T is non-Copy, custody transition. Failure changes nothing. Commit copies T from a structurally Copy carrier; otherwise it consumes the carrier and either transfers sole T custody or, when T itself is Copy, copies T. After either selection from a non-Copy carrier, the residual shell owns no child and is destroyed/deinitialized exactly once. Only the Ok path initializes the T operation result, and subsequent same-block operations may use it.

On Err, later same-block operations are skipped. It preflights only the exact edge scratch/bookkeeping, outer-carrier construction/accounting, result binding, and outbound-custody/handoff reservation. Failure leaves input, custody, path state, and loans unchanged and creates no scratch. Commit copies E from a structurally Copy carrier into a protected nonowning binding; otherwise it consumes/removes the carrier and either transfers sole non-Copy E custody to a derived non-addressable edge-private owner or copies a Copy E binding. After either selection from a non-Copy carrier, the empty residual shell is destroyed/deinitialized exactly once. No row, operand, path, loan, or recipe can name the protected binding/owner. The unique try-error edge then runs. Its recipes reverse-drop every prescribed other live owner and cannot name T, E, or produce a value. Only afterward is E copied or moved exactly once into the fresh outer Err carrier. If Result<U,E> is non-Copy, that completed carrier is appended to current- frame custody; a structurally Copy outer carrier has no owner custody. Entry loans remain live while ensures evaluate that normal early return. Successful outbound transfer removes non-Copy outer custody only afterward. The success path cannot access edge E, and the error path cannot access T. A postcommit drop/provider or ensures program/resource fault drops only the non-Copy scratch or outer carrier then present, plus the remaining frame, exactly once; outer construction and handoff themselves require no new fallible allocation after successful branch-specific preflight. The Ok path never traverses the error edge or its recipes.

Every tag-15 RETURN, including the certified Bytes.slice ephemeral return, is the terminal flow operation of its block and is reverse-bound to exactly one kind-three cleanup edge with that block as source and successor NONE. Ordinary value return then uses these custody rules. Before consuming or protecting the value, execution preflights edge bookkeeping, result binding, and outbound custody/handoff reservation. Failure leaves value, custody, path state, and loans unchanged. Commit moves a non-Copy return value into non-addressable protected result custody (or records the exact Copy value), then the edge recipes drop all other prescribed owners and cannot name that result. Ensures run with entry loans still live and the exact result binding when the contract subset admits it. Successful handoff removes protected custody only for a non-Copy owner; a Copy binding is simply discarded after publication. An ensures or postcommit fault drops only a protected non-Copy owner plus the remaining frame exactly once. The certified Bytes.slice return replaces only those ordinary value-custody/result-slot steps with its narrower bounded-loan handoff above; its hashed edge recipes and loan teardown remain mandatory.

Abrupt abort unwind is a separate deterministic frame rule, not a synthesized normal/error/control cleanup edge. After ownership commit, every rich-owner initialization, move into the frame, or reacquisition registers or reorders its exact current-frame custody in semantic initialization order fixed by the typed operations and owned-path facts. On a contract/body program fault or an engine execution-resource failure, active loans end child-before-parent in reverse dense creation/reborrow order, restoring each suspended exclusive parent before owner teardown, then all current frame owners recursively drop in reverse current acquisition order. Before ownership commit, caller owners remain untouched. Interpreter, emitted C, JIT, and AOT apply this identical rule. It does not authorize an engine to infer or omit any recorded normal, try-error, return, or control cleanup edge.

The conceptual custody list transition is exact. At entry ownership commit, moved runtime receiver/parameters are appended in logical runtime-slot order. A freshly constructed owner or nested-call result acquired by this frame is appended when its producing operation commits. A same-frame move into a newly initialized place or SSA result removes the old entry and appends the destination at that initialization/producer operation; it never duplicates custody. Only an explicitly specified pure metadata path relabel that creates no initialization may preserve list position. Moving an owner into a nested callee or outbound result removes it at that transfer’s commit; if a later result returns the same token, reacquisition appends a new entry. REPLACE_COMMIT removes/drops the old destination entry and retargets the already-constructed candidate entry without reordering that candidate. Normal explicit drop removes its entry. Recursive drop visits initialized fields in reverse semantic initialization ordinal and skips moved fields. Aggregate, variant, and rich-Result construction removes each consumed owned operand from top-level custody exactly when scratch assumes that field or payload, nests it exactly once, and appends the completed composite only at commit. A pre-commit fault leaves scratch owning only already-transferred fields and drops those fields in reverse semantic ordinal; no child remains in both the top-level list and a composite. FIELD_MOVE detaches the exact initialized nested field from its parent, marks that source field moved, and appends the extracted top-level SSA owner at the extraction operation’s commit. RESULT_TRY/RESULT_TRY_RICH follows the structural Copy split above: Copy carrier/payload bindings never enter owner custody; a non-Copy carrier is consumed once, and only a selected non-Copy payload assumes sole custody. On Err, edge-private scratch holds that owner (or the protected Copy binding), recipes run, and the payload is transferred once into the fresh outer Err. Only a non-Copy completed outer carrier is appended to current-frame custody before ensures. Precommit failure transfers nothing and creates no scratch; postcommit failure drops only actual non-Copy scratch/outer custody. Successful outbound handoff removes outer custody only after ensures. BYTE_BUILDER_FINISH is the explicit metadata-relabel exception: it retags its existing custody entry in place and does not change list position. Thus loop reinitialization, nested calls, replacement, and return have one cross-engine reverse-abort order rather than an ambient allocator order.

The schema-1.9 typed-operation record contains tag, exact result type or the no-result sentinel, a half-open operand-table range, two operation-specific unsigned 32-bit auxiliaries, flags, and a reserved zero word. Every operand names an exact typed SSA value or typed place; the validator never infers its type from a host stack word. Tags 27, 28, and 30–34 are noncanonical in schema 1.9 and retain their meanings only in prior schemas. Generalized tags are UNIT_VALUE 35, AGGREGATE_CONSTRUCT 36, FIELD_COPY 37, FIELD_MOVE 38, PLACE_MOVE 39, PLACE_DROP 40, BORROW_SHARED 41, BORROW_MUT 42, BORROW_SLICE_BYTE 43, RESULT_OK_RICH 44, RESULT_ERR_RICH 45, RESULT_TRY_RICH 46, INTRINSIC_CALL 47, REPLACE_COMMIT 48, SHIFT_LEFT 49, and SHIFT_RIGHT 50, VARIANT_CONSTRUCT 51, and BYTE_BUILDER_FINISH 52. An intrinsic call names an exact catalog-function ID and effect-set digest through semantic-symbol references. The header and logical module identities separately bind the selected catalog content identity.

Rich Result construction stores one exact logical T or E payload and an independent zero/one tag; it is not the schema-1.7 high-32-bit packing. Rich try follows the structural Copy split above: a Copy carrier/payload is selected as a Copy binding, only a non-Copy carrier is consumed, and only a selected non-Copy payload transfers owner custody. On Err it follows the recorded error cleanup edge, copies or moves E once into a fresh outer carrier, and returns only after all pending drops and ensures. Never makes the corresponding variant uninhabited rather than manufacturing a payload.

Schema-1.9 aggregate operations carry logical typed values. An implementation may represent a live rich owner by an opaque runtime handle scoped to one bounded execution context, but that handle is not a ZLM value or semantic identity. It is never serialized, reflected, compared, or accepted by another context. Aggregate construction initializes fields left to right. Field moves update exact move paths. Recursive drop releases initialized fields in reverse order. REPLACE_COMMIT is valid only after a fully initialized replacement exists; an error before it leaves the old destination initialized.

A module uses schema 1.9 exactly when it needs a new table, type instance, generalized operation, multiple declaration, general field, nonempty effect, loan, or rich payload that schemas 1.2–1.8 cannot represent. An empty effect set or a fact already representable in a prior schema does not promote the artifact. Otherwise the writer selects the same lowest canonical prior schema as before. All schema 1.9 additions are append-only with respect to the format family, and schemas 1.2–1.8 remain byte-for-byte stable. A 1.9 reader does not reinterpret a legacy schema or synthesize absent rich records.

C0-ART-004 — Separate ancillary data. Source maps, prose provenance, compiler/build provenance, and target materialization records are separate hash-addressed sections. Their bytes do not affect target-independent semantic identity.

C0-ART-005 — Compatibility. Schema-major changes require a new magic or major identifier. The bootstrap retains a ZLM0 reader while migration tests exist; a reader never guesses a schema from payload shape.

Execution and reflection

C0-EXEC-001 — One semantics. The checked interpreter is the executable reference. A deterministic C or LLVM materializer consumes the same validated Core IR and must preserve its evaluation, ownership, cleanup, errors, contracts, dispatch, and numeric preset.

C0-EXEC-002 — Backend boundary. A materializer is not a second language frontend. It accepts only a serialized checked package plus explicit target configuration and rejects unsupported or malformed operations rather than inventing source semantics.

C0-EXEC-003 — Explicit target. Native output identity includes target triple, CPU baseline, enabled features, optimization, relocation model, code model, backend version, linker identity, and host ABI version. Ambient host CPU features cannot enter a reproducible build.

Stage0 exposes zl_llvm_emit_object_for_target_v1 for the materializer-owned portion of this record. It consumes caller-supplied triple, CPU, feature, optimization, relocation, and code-model fields and never queries host CPU capabilities. The shorter zl_llvm_emit_object API discovers LLVM’s default triple and is therefore a local convenience, not reproducibility or bootstrap evidence. Backend/linker/host-ABI identities remain the surrounding build record’s responsibility.

C0-REFL-001 — Semantic reflection. Canonical reflection exposes modules, public and retained private semantic IDs, types, messages, domains, effects, contracts, ownership signatures, dispatch contracts, numeric preset, verification state, and authority/evidence identities. It excludes source formatting from semantic identity.

C0-REFL-002 — No authority creation. Reflection describes accepted checked semantics; it cannot regenerate or supersede .zl.md/.zli.md authority and does not grant ambient access to live objects or mutable fields.

Determinism

C0-DET-001 — Canonical order. Maps, sets, declarations, diagnostics, interfaces, reflection, symbols, and link manifests have specification-defined ordering independent of hash-table iteration, threads, filesystem enumeration, locale, absolute path, and process identity.

C0-DET-002 — Stable fixed point. Rebuilding identical accepted source with the same compiler semantics produces byte-identical source-map-free checked payloads, .zli, reflection, protocol catalogs, and canonical emitted C. Native object equality is required only by an explicitly pinned native reproducibility profile.

C0-DET-003 — Cryptographic identities. Trusted content identities use domain-separated SHA-256 over canonical bytes. The provisional FNV identities in the current runtime are not bootstrap trust identities.

Projected fromspec/editions/core-0/checked-artifacts-and-execution.md