Specialization R0-A Encoding v1

Status: implemented and vector-locked
Authority: ADR-0023
Scope: canonical P1V0 static values, R0 policy, request identity, and admission

1. Purpose

R0-A is the trust boundary between verified B0 evidence and future static evaluation. It admits only exact, typed static facts and value-free dynamic holes. It performs no Core evaluation and emits no Residual Core.

The encoding is independent of Rust enum layout, Arc, pointer width, collection capacity, memory address, and host endianness.

2. Scalar framing

R0-A uses the Core-N0 canonical scalar rules:

• U16, U32, and U64 are unsigned big-endian;
• I64 is 64-bit two’s-complement big-endian;
• enum and Boolean tags are one byte;
• a sequence is U32 element_count followed by its elements;
• a string is U32 byte_length followed by UTF-8 bytes;
• an embedded canonical value is U32 byte_length followed by all its bytes;
• a length greater than U32::MAX fails encoding.

F64 uses big-endian IEEE-754 bits. Every NaN is normalized to 0x7ff8000000000000; positive and negative zero remain distinct.

All identities in this document are SHA-256 digests of their complete canonical payload.

3. Static-value identity

Canonical value payloads begin with:

NAUX:core-n0:specialization-value:r0:v1\0

Value tags and following fields are:

The sum-type encoding is the one defined by Core-N0 Semantic Encoding v1: sum name, then the ordered sequence of constructor names and field types.

The locked value vector is:

Tuple([
  I64(7),
  F64(-0.0),
  ArrayF64([1.5, NaN])
])

value_hash =
a06da2023df1cafbf7e214af56848587a5e2fa6f134f6527da06d1416f2282a8

Changing a NaN payload preserves this identity. Changing -0.0 to +0.0, field order, a tag, a sum identity, array length, or an element changes it.

4. Policy identity

Canonical policy payloads begin with:

NAUX:core-n0:specialization-policy:r0:v1\0

Fields occur in this exact order:

Core schema name string
Core schema version: U16, U16, U16
R0 policy version: U16, U16, U16
Core profile tag
P1V0 interpreter_semantics_hash: 32 bytes
B0 policy_hash: 32 bytes
max static-value nodes hard cap: U64
max static-array elements hard cap: U64
max specialization steps hard cap: U64
max residual nodes hard cap: U64
max residual bytes hard cap: U64
capability string sequence

Version and hard caps:

R0 policy version                 = 1.0.0
max static-value nodes            = 1,000,000
max static-array elements         = 16,777,216
max specialization steps          = 100,000,000
max residual nodes                = 1,000,000
max residual bytes                = 1,073,741,824

Capabilities occur in this exact order:

verified-b0-certificate-only-v1
exact-static-dynamic-entry-slots-v1
canonical-immutable-p1v0-values-v1
effect-safe-static-execution-required-v1
fail-closed-specialization-budgets-v1
verified-residual-core-only-v1

Locked policy vector:

policy payload bytes = 404

policy_hash =
f4bb6684d043f693229140f200deb1bcee04f147ef92cb88fd07421c7ae6c1c7

5. Request identity

Canonical request payloads begin with:

NAUX:core-n0:specialization-request:r0:v1\0

Fields occur in this exact order:

request schema version: U16, U16, U16
source_program_hash: 32 bytes
interpreter_semantics_hash: 32 bytes
B0 policy version: U16, U16, U16
B0 policy_hash: 32 bytes
B0 request_hash: 32 bytes
B0 certificate_hash: 32 bytes
R0 policy version: U16, U16, U16
R0 policy_hash: 32 bytes
entry FunctionId: U32
entry specialization-slot sequence
max static-value nodes: U64
max static-array elements: U64
max specialization steps: U64
max residual nodes: U64
max residual bytes: U64

Request schema v1 is 1.0.0.

Slot tags are:

The embedded static value includes its own value domain. A dynamic slot has no example, profile, guard, or fallback value.

6. Admission

Validation first independently verifies the supplied B0 certificate. It then requires exact equality for all source, interpreter, B0, R0-policy, entry, slot, type, and budget fields.

Recursive static-value checking admits only:

Unit
Bool
I64
F64
Tuple
Sum
read-only Array<F64>

Each aggregate and scalar consumes one static-value node. An array consumes one value node and separately consumes its number of elements. All five budgets must be non-zero, no larger than their policy hard cap, and are part of request identity. Admission is fail-closed; hashing an unvalidated request does not validate it.

The validated wrapper retains the exact source artifact, verified B0 certificate, canonical request, and request hash. It is the only value R0-B code may accept, preventing a validated request from being paired with a different artifact after admission. R0-B1 follows this boundary.

7. Locked request vector

The vector source contains one pure entry function:

function 0(local 0: I64, local 1: F64) -> I64
  return local 0

Its B0 manifest is [Static, Dynamic] with budgets 1000 nodes, 100 call edges, and 20 fixed-point iterations. Its R0 slots and budgets are:

[Static(I64(7)), Dynamic(F64)]

max static-value nodes    = 100
max static-array elements = 100
max specialization steps  = 10,000
max residual nodes        = 1,000
max residual bytes        = 1,000,000

Locked provenance and identity:

source_program_hash =
41dec113d32aba3a4e5604274aa6e2cc28defe8b6c225e80c48bdf2b5fce9d81

interpreter_semantics_hash =
d9911cf60e5afa54e271cdff274cde41b522a4a0c9855ccd6efbcd4e981909cc

B0 policy_hash =
ee19444d56fe1de89eab9a0054c556b47e7ad115ec12255511d31a4526261a51

B0 request_hash =
d8dbe5ff2b3270547e1c70632b5da714145c77fe5d7e97321042189aa36d7d60

B0 certificate_hash =
341439f633487f5fc2f194a23e85e6a1b95f2a8476ddf810410389ddc6ab2601

request payload bytes = 356

request_hash =
d2735a25744b9087ee1efd18f2182c78d4bf831eae1bb274bb9ebeca5e640b44

Any payload-order, framing, tag, policy, provenance, slot, type, or budget change must preserve these vectors or introduce a new version/domain.

8. Non-claims

R0-A executes no static term, handles no effect, produces no residual term, and proves no original/residual equivalence. It is not R0-B/C/D, CoreVM0, Futamura P1/P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis.