amduat/tier1/opreg-pel1-kernel-params-1.md
2025-12-22 12:17:40 +01:00

17 KiB
Raw Permalink Blame History

OPREG/PEL1-KERNEL-PARAMS/1 — Kernel Operation Parameter Encodings

Status: Approved Owner: Niklas Rydberg Version: 0.1.3 SoT: Yes Last Updated: 2025-12-22 Linked Phase Pack: N/A Tags: [registry, binary-minimalism]

Document ID: OPREG/PEL1-KERNEL-PARAMS/1 Layer: L1 Profile (Parameter Encoding for OPREG/PEL1-KERNEL)

Depends on (normative):

  • ASL/1-CORE v0.3.xArtifact, TypeTag, Reference, HashId
  • HASH/ASL1 v0.2.x — ASL1 hash family (for HashId constraints)
  • OPREG/PEL1-KERNEL v0.1.3 — kernel operation semantics

Integrates with (informative):

  • PEL/PROGRAM-DAG/1 — DAG program scheme (Node parameters)
  • PEL/1-CORE — primitive execution semantics

© 2025 Niklas Rydberg.

License

Except where otherwise noted, this document (text and diagrams) is licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0).

The identifier registries and mapping tables (e.g. TypeTag IDs, HashId assignments, EdgeTypeId tables) are additionally made available under CC0 1.0 Universal (CC0) to enable unrestricted reuse in implementations and derivative specifications.

Code examples in this document are provided under the Apache License 2.0 unless explicitly stated otherwise. Test vectors, where present, are dedicated to the public domain under CC0 1.0.


0. Purpose and Scope

OPREG/PEL1-KERNEL-PARAMS/1 defines the canonical binary encodings for the logical Params types used by the kernel operations in OPREG/PEL1-KERNEL v0.1.1:

  • pel.bytes.concat/1
  • pel.bytes.slice/1
  • pel.bytes.const/1
  • pel.bytes.hash.asl1/1
  • pel.bytes.params/1

It specifies, for each operation:

  1. The logical Params value type (e.g. SliceParams).

  2. The canonical encoding function:

    encode_params(OpParams) -> OctetString
    
  3. The canonical decoding function:

    decode_params(OctetString) -> OpParams | error
    
  4. How decode errors must be treated in the context of PEL/PROGRAM-DAG/1 (always as INVALID_PROGRAM for these kernel ops).

This document is deliberately independent of any Program encoding format. A Program representation (e.g. ENC/PEL-PROGRAM-DAG/1) simply needs to:

  • store the operations Params as an opaque OctetString, and
  • feed that OctetString into the encoders/decoders defined here.

For each Params type, the encoding defined here is the only canonical encoding; engines MUST NOT accept alternative layouts.


1. Conventions

1.1 Base types

From ASL/1-CORE:

OctetString = finite sequence of bytes (0x000xFF)

HashId = uint16

In this document, OctetString is the logical type sequence of bytes. When we encode an OctetString as part of Params (e.g. ConstParams.bytes), we use [u64 length][bytes].

This document introduces the following fixed-width integer types:

u8   = unsigned  8-bit integer
u16  = unsigned 16-bit integer
u32  = unsigned 32-bit integer
u64  = unsigned 64-bit integer

1.2 Byte order and integer encoding

All multi-byte integers in parameter encodings are encoded:

  • as big-endian (most significant byte first),
  • using a fixed width (1, 2, 4, or 8 bytes).

Conversions:

  • u16 → 2 bytes
  • u32 → 4 bytes
  • u64 → 8 bytes

1.3 Boolean encoding

Booleans are encoded as:

false -> 0x00
true  -> 0x01

Any other value is invalid and MUST be treated as a decode error.

1.4 OctetString encoding (embedded)

When an OctetString is encoded as part of Params, it uses:

[length: u64] [bytes: b[length]]
  • length is the number of bytes.
  • length MAY be zero.
  • There is no terminator or padding.

1.5 Param payload

For each Node in a Program, the scheme-level “Params” field is represented as an OctetString params_bytes.

This document defines, for kernel operations, what it means for params_bytes to represent:

  • Unit (no parameters),
  • SliceParams,
  • ConstParams,
  • HashParams.

Other operations (non-kernel) may use other param-encoding profiles.

1.6 Error handling model

For all kernel operations:

Any param decode error MUST be treated as a static program error (INVALID_PROGRAM) in PEL/PROGRAM-DAG/1, not as a runtime error.

Concretely:

  • If decode_params fails for a Node during Program validation, Exec_DAG MUST treat the Program as invalid and produce status = INVALID_PROGRAM, not RUNTIME_FAILED.

1.7 Relationship to ENC/PEL-PROGRAM-DAG/1 and size bounds

In contexts that use ENC/PEL-PROGRAM-DAG/1, each Node carries an operation-specific parameter payload in its params_bytes field. For kernel operations defined in OPREG/PEL1-KERNEL:

  • The params_bytes field of a Node MUST be exactly the byte sequence returned by the corresponding encode_params_* function for that Nodes operation.
  • Engines validating or executing a PEL/PROGRAM-DAG/1 Program MUST feed params_bytes into the matching decode_params_* function for that operation.

Because ENC/PEL-PROGRAM-DAG/1 represents params_bytes with a params_len : u32 length prefix, all encode_params_* functions defined in this document MUST produce parameter payloads whose length is ≤ 0xFFFF_FFFF (2³² 1) bytes. Any logical parameter value that would require a larger encoding MUST either:

  • be rejected at parameter construction time, or
  • be represented via separate input Artifacts instead of being inlined as Node parameters.

For kernel operations, any failure to decode params_bytes with the corresponding decode_params_* function (including violations of the size bound above) MUST be reported to the PEL/PROGRAM-DAG/1 layer as a parameter-decoding error and treated as an invalid Program, not as a runtime failure during execution.


2. Operation Param Types (Logical)

For reference (from OPREG/PEL1-KERNEL):

// pel.bytes.concat/1
ConcatParams = Unit

// pel.bytes.params/1
ParamsParams = Unit

// pel.bytes.slice/1
SliceParams {
  offset: u64
  length: u64
}

// pel.bytes.const/1
ConstParams {
  bytes:   OctetString
  has_tag: bool
  tag_id:  u32 optional  // only meaningful when has_tag = true
}

// pel.bytes.hash.asl1/1
HashParams {
  hash_id: HashId   // uint16
}

This specification does not change these logical types; it only provides their canonical encodings.


3. Unit Params Encoding (pel.bytes.concat, pel.bytes.params)

Applies to:

  • pel.bytes.concat/1
  • pel.bytes.params/1

3.1 Logical type

Unit = ()

There is a single value.

3.2 Encoding

encode_params_unit(Unit) -> OctetString

Definition:

encode_params_unit(()) = ""   // zero-length OctetString

That is, params_bytes MUST be an empty byte sequence.

3.3 Decoding

decode_params_unit(params_bytes: OctetString) -> Unit | error

Algorithm:

  1. If len(params_bytes) != 0:

    • return error.
  2. Otherwise:

    • return ().

3.4 Conformance rule

For pel.bytes.concat/1 and pel.bytes.params/1:

  • params_bytes MUST be encoded using encode_params_unit.
  • Any non-empty params_bytes MUST be treated as a decode error and thus INVALID_PROGRAM in PEL/PROGRAM-DAG/1.

4. SliceParams Encoding (pel.bytes.slice)

Applies to:

  • pel.bytes.slice/1

4.1 Logical type

SliceParams {
  offset: u64   // 0-based byte offset
  length: u64   // number of bytes
}

4.2 Encoding

encode_params_slice(SliceParams) -> OctetString

Given:

SliceParams { offset, length }

The encoding is:

[offset: u64] [length: u64]

where both offset and length are encoded as big-endian u64.

So:

  • Total length of params_bytes MUST be exactly 16 bytes.

4.3 Decoding

decode_params_slice(params_bytes: OctetString) -> SliceParams | error

Algorithm:

  1. If len(params_bytes) != 16:

    • return error.
  2. Parse the first 8 bytes as offset: u64 (big-endian).

  3. Parse the next 8 bytes as length: u64 (big-endian).

  4. Construct:

    SliceParams { offset, length }
    

    and return it.

This decoding does not apply any semantic checks on offset or length (such as “must be in range for a particular input”). Those checks are done at operation runtime and mapped to RANGE_OUT_OF_BOUNDS (status_code = 0x0002_0001) as specified in OPREG/PEL1-KERNEL.

4.4 Conformance rule

  • params_bytes for a pel.bytes.slice/1 Node MUST be exactly 16 bytes, encoded as described.
  • Any other length or malformed encoding MUST be treated as a decode errorINVALID_PROGRAM.

5. ConstParams Encoding (pel.bytes.const)

Applies to:

  • pel.bytes.const/1

5.1 Logical type

ConstParams {
  bytes:   OctetString
  has_tag: bool
  tag_id:  u32 optional
}

Semantics:

  • If has_tag == false:

    • The output Artifact will have type_tag = None.
  • If has_tag == true:

    • The output Artifact will have type_tag = Some(TypeTag{ tag_id }).

5.2 Encoding

encode_params_const(ConstParams) -> OctetString

Given:

ConstParams { bytes = B, has_tag, tag_id? }

The encoding is:

[has_tag: u8] [tag_id: u32?] [len: u64] [B: b[len]]

Where:

  1. has_tag: u8

    • 0x00 if has_tag == false.
    • 0x01 if has_tag == true.
  2. tag_id: u32 (only when has_tag == true)

    • Encoded as big-endian u32.
    • Omitted entirely when has_tag == false.
  3. len: u64

    • Length in bytes of B.
    • Encoded as big-endian u64.
  4. B: b[len]

    • The raw bytes of the payload.

So:

  • If has_tag == false, layout is:

    [0x00] [len: u64] [B: b[len]]
    
  • If has_tag == true, layout is:

    [0x01] [tag_id: u32] [len: u64] [B: b[len]]
    

5.3 Decoding

decode_params_const(params_bytes: OctetString) -> ConstParams | error

Algorithm:

  1. If len(params_bytes) < 1:

    • return error.
  2. Read the first byte as flag: u8.

    • If flag == 0x00, then has_tag = false.
    • If flag == 0x01, then has_tag = true.
    • Otherwise (any other value): return error.
  3. If has_tag == false:

    1. Ensure at least 1 + 8 bytes are present:

      • If len(params_bytes) < 1 + 8: return error.
    2. Parse the next 8 bytes as len: u64 (big-endian).

    3. Compute expected_total = 1 + 8 + len.

      • If len(params_bytes) != expected_total: return error.
    4. Let B be the remaining len bytes.

    5. Return:

      ConstParams {
        bytes   = B
        has_tag = false
        tag_id  = (absent)
      }
      
  4. If has_tag == true:

    1. Ensure at least 1 + 4 + 8 bytes are present:

      • If len(params_bytes) < 1 + 4 + 8: return error.
    2. Parse next 4 bytes as tag_id: u32 (big-endian).

    3. Parse next 8 bytes as len: u64 (big-endian).

    4. Compute expected_total = 1 + 4 + 8 + len.

      • If len(params_bytes) != expected_total: return error.
    5. Let B be the remaining len bytes.

    6. Return:

      ConstParams {
        bytes   = B
        has_tag = true
        tag_id  = tag_id
      }
      

5.4 Conformance rule

  • For pel.bytes.const/1, params_bytes MUST be encoded according to encode_params_const.
  • Any malformed encoding (invalid has_tag, truncated data, mismatched length, etc.) MUST be treated as a decode errorINVALID_PROGRAM.

6. HashParams Encoding (pel.bytes.hash.asl1)

Applies to:

  • pel.bytes.hash.asl1/1

6.1 Logical type

HashParams {
  hash_id: HashId   // uint16
}

6.2 Encoding

encode_params_hash(HashParams) -> OctetString

Given:

HashParams { hash_id }

The encoding is:

[hash_id: u16]

Where:

  • hash_id is encoded as big-endian u16.

So params_bytes MUST be exactly 2 bytes.

6.3 Decoding

decode_params_hash(params_bytes: OctetString) -> HashParams | error

Algorithm:

  1. If len(params_bytes) != 2: return error.

  2. Parse the 2 bytes as hash_id: u16 (big-endian).

  3. For pel.bytes.hash.asl1/1 in this version:

    • If hash_id != 0x0001:

      • return error.
    • Else:

      • return HashParams { hash_id }.

Rationale:

  • OPREG/PEL1-KERNEL constrains pel.bytes.hash.asl1/1 to hash_id = 0x0001 (HASH-ASL1-256) for cross-implementation determinism.
  • Supporting additional HashIds requires a new operation version (e.g. pel.bytes.hash.asl1/2) and/or an updated parameter profile.

6.4 Conformance rule

  • For pel.bytes.hash.asl1/1, params_bytes MUST:

    • be exactly 2 bytes long, and
    • encode hash_id = 0x0001.
  • Any other length or hash_id MUST be treated as a decode errorINVALID_PROGRAM.


7. Integration with PEL/PROGRAM-DAG/1 (Informative)

In a PEL/PROGRAM-DAG/1 Program:

  • Each Node has:

    • an OperationId { name, version }, and
    • a params_bytes: OctetString (representation-specific; this spec does not define the layout of the Node itself).
  • For Nodes whose OperationId is one of the kernel ops from OPREG/PEL1-KERNEL:

    • The engine MUST:

      1. Select the appropriate decode_params_* function from this document based on OperationId.name and version.

      2. Pass params_bytes to that function.

      3. If decoding fails, treat the Program as INVALID_PROGRAM as per PEL/PROGRAM-DAG/1:

        ExecutionStatus      = INVALID_PROGRAM
        ExecutionErrorKind   = PROGRAM
        summary.status_code  = 2
        
      4. If decoding succeeds, use the resulting Params value for the operation semantics.

  • For non-kernel operations, other param profiles apply; they MUST NOT conflict with these definitions.


8. Conformance

An implementation is OPREG/PEL1-KERNEL-PARAMS/1conformant if and only if:

  1. Encoding/decoding correctness

    • For each kernel operation:

      • encode_params_* and decode_params_* are implemented exactly as specified.

      • For all valid Params values:

        decode_params_*(encode_params_*(value)) == value
        
      • For all params_bytes accepted by decode_params_*, the result is well-defined and deterministic.

  2. Error handling

    • Any malformed or non-canonical params_bytes detected by decode_params_* is treated as a decode error.
    • Decode errors for kernel operations MUST be mapped to INVALID_PROGRAM in PEL/PROGRAM-DAG/1, not RUNTIME_FAILED.
  3. Consistency with OPREG/PEL1-KERNEL

    • The logical Params types used in the engines implementation of kernel operations match those defined in OPREG/PEL1-KERNEL.
    • Runtime failures for kernel operations are not caused by param decode errors; they are caused only by data-dependent conditions specified in OPREG/PEL1-KERNEL (e.g. slice out-of-bounds).
  4. Determinism

    • For any given params_bytes, decode_params_* MUST return the same result (or error) across all conformant implementations.
  5. Layering

    • The implementation does not depend on any particular Program encoding.
    • It only consumes params_bytes as an OctetString and produces/consumes logical Params as defined here.

9. Change Log (Informative)

v0.1.3 (2025-12-22)

  • Updated the dependency to OPREG/PEL1-KERNEL v0.1.3; no encoding changes.

v0.1.2 (2025-12-22)

  • Added pel.bytes.params/1 to the unit-params encoding scope, aligned to OPREG/PEL1-KERNEL v0.1.2.

v0.1.1 (2025-11-15)

  • Aligned with OPREG/PEL1-KERNEL v0.1.1:

    • Removed pel.bytes.clone/1 from the normative scope of this profile; the kernel parameter profile now covers only:

      • pel.bytes.concat/1
      • pel.bytes.slice/1
      • pel.bytes.const/1
      • pel.bytes.hash.asl1/1
    • Updated the informative reference in §4.3 so that RANGE_OUT_OF_BOUNDS now points to status_code = 0x0002_0001, reflecting the reassigned kernel_op_code for pel.bytes.slice/1.

    • Clarified the dependency on OPREG/PEL1-KERNEL v0.1.1 in the header.

v0.1.0 (2025-11-15)

  • Introduced canonical parameter encodings for:

    • pel.bytes.clone/1 (Unit → empty params_bytes)
    • pel.bytes.concat/1 (Unit → empty params_bytes)
    • pel.bytes.slice/1 (SliceParams { offset, length } → 16-byte payload)
    • pel.bytes.const/1 (ConstParams[has_tag][tag_id?][len][bytes])
    • pel.bytes.hash.asl1/1 (HashParams { hash_id } → 2-byte payload; restricted to 0x0001)
  • Locked the rule that all kernel param decode failures imply INVALID_PROGRAM, not runtime failure.

  • Kept the profile independent from any particular Program encoding (ENC/PEL-PROGRAM-DAG/1).


Document History

  • 0.1.3 (2025-12-22): Updated kernel dependency version reference.
  • 0.1.2 (2025-12-22): Added pel.bytes.params/1 to the kernel params profile.
  • 0.1.1 (2025-11-16): Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.