Core-N0 Semantic Encoding v1

Status: implemented for profiles P1V0, P1V1, P1V2, P1V3, P1V4, and P1V5
Schema: core-n0 0.1.0
Domain: NAUX:core-n0:semantic:v1\0
Digest: SHA-256

1. Purpose

This encoding gives a Core-N0 program a deterministic, host-independent byte representation and semantic hash. It is used for artifact admission, provenance, reproducibility, and independent checking.

The encoding is not Rust serialization. It does not encode Rust enum layout, pointer width, collection capacity, debug names, memory addresses, or host endianness.

2. Scalar framing

• Integers are unsigned big-endian unless the field is explicitly I64.
• I64 is encoded as its 64-bit two’s-complement big-endian representation.
• Every sequence is U32 length followed by its elements.
• Every UTF-8 string is U32 byte_length followed by its bytes.
• A sequence or string longer than U32::MAX fails encoding.
• Enum discriminants are one byte.
• IDs are encoded as U32.

An F64 literal is encoded as big-endian IEEE-754 bits. All NaNs are canonicalized to 0x7ff8000000000000 because Core-N0 v0.1 does not observe NaN payloads. Signed zero is not canonicalized.

3. Program envelope

Fields occur in this exact order:

domain bytes
schema name
schema major: U16
schema minor: U16
schema patch: U16
profile tag
entry FunctionId
functions sequence

The artifact’s declared semantic hash is not part of the hashed bytes:

semantic_hash = SHA256(semantic_bytes(program))

Profile tags:

4. Function encoding

FunctionId
region_parameters sequence of RegionId
parameters sequence of (LocalId, Type)
EffectRow
result Type
body Term

Functions and region parameters must be strictly increasing. Effect rows must be strictly sorted and duplicate-free. The verifier rejects rather than normalizes non-canonical artifacts.

5. Type tags

Mutability tags are Read = 0, Unique = 1, and Shared = 2.

A sum type is:

sum name
constructors sequence

Each constructor is its name followed by its field-type sequence.

Schema representation does not imply profile admission. P1V0 rejects Text, Bytes, Ref, Function, Closure, and every array except read-only Array<F64>. P1V1 additionally admits only non-escaping Ref<rho, Shared, Bool|I64|F64>. P1V2 additionally admits bounded non-escaping Closure values whose behavioral parameters and result contain neither references nor closures. P1V3 additionally admits typed user operations and affine implicit lexical handlers. P1V4 additionally admits direct non-escaping Ref<rho, Unique, Bool|I64|F64> owners with verifier-checked affine move and borrow semantics; aggregate and capture containment remains rejected. P1V5 additionally admits one direct unique result on an internal function when exactly one matching direct unique parameter anchors its region and every other parameter is reference-free.

6. Effect encoding

Error-kind tags:

P1V0 admits only Error<Overflow> and Error<Bounds>. P1V1 and P1V2 additionally admit State<rho> and Alloc<rho> when rho is a declared function region. P1V3, P1V4, and P1V5 additionally admit Operation<signature>.

An operation signature is:

OperationId
parameter-type sequence
result Type

7. Operand and numeric encoding

Operand tags:

Numeric-mode tags are Checked = 0, Wrapping = 1, and Saturating = 2.

Primitive tags:

8. RValue encoding

9. Term encoding

Each case arm is:

U32 constructor index
binding LocalId sequence
body Term

Arms must be exhaustive and appear once in constructor-index order.

Each handler clause is:

operation signature
parameter LocalId sequence
clause body Term

Handler clauses must be non-empty and strictly ordered by OperationId.

10. Stability vector

The P1V0 program containing one pure entry function 0 that returns the literal F64(42.0) has semantic hash:

4d7afe3c5d1127e7b8ce1441c21edb8322d99480ff7efbb5051e6a73d3930bcf

This vector is enforced by the Rust seed tests. A future semantic encoding change to an existing tag, field order, normalization rule, or domain requires a new domain/version, an ADR, migration policy, verifier update, and new stability vectors. A new profile may use previously unassigned append-only tags; older decoders must reject its unknown profile tag.

The P1V1 alias program locked by the logical-store contract has semantic hash:

ac526f04cef5428c41b002f978ff52f7eab3752bbee98d564e67f84b5edde5a6

The P1V2 value-closure program locked by the existential-closure contract has semantic hash:

ba1613399e67b828b1e629ace2236d492ae86b01d7a2c8ecd7304d27ae763e75

The P1V3 capture-and-resume program locked by the linear-handler contract has semantic hash:

20f4ae704987e1b61795085575c622111fb290dd72655899dcb770fa8a6723b4

The P1V4 repeated-borrow program locked by the affine-unique contract has semantic hash:

f314f6e72535bf12b6b42aa962a4a34c70845a7eefa709e7242b190b95fa27a9

The P1V5 mutate-and-return program locked by the ownership-return contract has semantic hash:

09006d69756a52fd1fe1dfc36cd198d1a40122a5201fbcfe73ccd6d538a9290a