amduat/tier1/opreg-pel1-kernel-params-1.md

# 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]

<!-- Source: /amduat/docs/new/opreg-pel1-kernel-params-1.md | Canonical: /amduat/tier1/opreg-pel1-kernel-params-1.md -->

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

**Depends on (normative):**

* `ASL/1-CORE v0.3.x` — `Artifact`, `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:

   ```text
   encode_params(OpParams) -> OctetString
   ```

3. The **canonical decoding** function:

   ```text
   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 operation’s 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`:

```text
OctetString = finite sequence of bytes (0x00–0xFF)

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:

```text
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:

```text
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:

```text
[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 Node’s 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 `Artifact`s 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`):

```text
// 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

```text
Unit = ()
```

There is a single value.

### 3.2 Encoding

```text
encode_params_unit(Unit) -> OctetString
```

Definition:

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

That is, `params_bytes` MUST be an empty byte sequence.

### 3.3 Decoding

```text
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

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

### 4.2 Encoding

```text
encode_params_slice(SliceParams) -> OctetString
```

Given:

```text
SliceParams { offset, length }
```

The encoding is:

```text
[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

```text
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:

   ```text
   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 error** ⇒ `INVALID_PROGRAM`.

---

## 5. ConstParams Encoding (`pel.bytes.const`)

Applies to:

* `pel.bytes.const/1`

### 5.1 Logical type

```text
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

```text
encode_params_const(ConstParams) -> OctetString
```

Given:

```text
ConstParams { bytes = B, has_tag, tag_id? }
```

The encoding is:

```text
[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:

  ```text
  [0x00] [len: u64] [B: b[len]]
  ```

* If `has_tag == true`, layout is:

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

### 5.3 Decoding

```text
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:

      ```text
      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:

      ```text
      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 error** ⇒ `INVALID_PROGRAM`.

---

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

Applies to:

* `pel.bytes.hash.asl1/1`

### 6.1 Logical type

```text
HashParams {
  hash_id: HashId   // uint16
}
```

### 6.2 Encoding

```text
encode_params_hash(HashParams) -> OctetString
```

Given:

```text
HashParams { hash_id }
```

The encoding is:

```text
[hash_id: u16]
```

Where:

* `hash_id` is encoded as big-endian `u16`.

So `params_bytes` MUST be exactly 2 bytes.

### 6.3 Decoding

```text
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 `HashId`s 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 error** ⇒ `INVALID_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`:

       ```text
       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/1–conformant** 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:

       ```text
       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 engine’s 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.