pel: require params for pel.bytes.params and add test
This commit is contained in:
Carl Niklas Rydberg
parent
d0005e54c3
commit
a932363ad0
30
AUDITS.md
30
AUDITS.md
|
|
@ -41,8 +41,8 @@ Status legend: ✅ completed, ⬜ pending.
|
|||
13. ✅ `tier1/tgk-1-core.md`
|
||||
14. ✅ `tier1/enc-tgk1-edge-1.md`
|
||||
15. ✅ `tier1/tgk-store-1.md`
|
||||
16. ⬜ `tier1/tgk-prov-1.md`
|
||||
17. ⬜ `tier1/opreg-pel1-kernel.md`
|
||||
16. ✅ `tier1/tgk-prov-1.md`
|
||||
17. ✅ `tier1/opreg-pel1-kernel.md`
|
||||
18. ⬜ `tier1/opreg-pel1-kernel-params-1.md`
|
||||
19. ⬜ `tier1/opreg-tgk-docgraph-1.md`
|
||||
20. ⬜ `tier1/amduat20-stack-overview.md`
|
||||
|
|
@ -225,3 +225,29 @@ Status legend: ✅ completed, ⬜ pending.
|
|||
- Resolution: mapped conflicting artifacts during `resolve_edge` to
|
||||
`GS_ERR_ARTIFACT_ERROR` to match artifact-level integrity error handling.
|
||||
- Tests: user reported “100% tests passed, 0 tests failed out of 14”.
|
||||
|
||||
## 2025-12-22 — TGK/PROV/1 (`tier1/tgk-prov-1.md`)
|
||||
- Scope: provenance query parameters, closure/depth/layer semantics, and trace
|
||||
graph construction over TGK/1-CORE projections.
|
||||
- Findings: no gaps found; `prov_closure_nodes`, `prov_depths`, `prov_layers`,
|
||||
and `prov_trace` follow TGK/PROV/1 semantics, including seed handling,
|
||||
payload non-traversal, depth limits, and trace node/edge construction.
|
||||
- Resolution: none required.
|
||||
- Tests: not run (tgk provenance tests exist under `tests/tgk/test_tgk_prov.c`).
|
||||
|
||||
## 2025-12-22 — OPREG/PEL1-KERNEL (`tier1/opreg-pel1-kernel.md`)
|
||||
- Scope: kernel op registry entries, runtime status codes, diagnostics
|
||||
requirements, and Params/arity enforcement for the four kernel ops.
|
||||
- Findings: `pel.bytes.params` is registered as a kernel op with
|
||||
`kernel_op_code = 0x0005` but is not listed in the OPREG/PEL1-KERNEL registry;
|
||||
`amduat_pel_program_dag_exec` attaches diagnostics for kernel op runtime
|
||||
failures even though the spec mandates an empty diagnostics list for kernel
|
||||
ops; internal/invalid artifact handling can yield `status_code = 1` or
|
||||
`AMDUAT_PEL_KERNEL_STATUS_INTERNAL`/`AMDUAT_PEL_KERNEL_STATUS_OOM`, which do
|
||||
not follow the `kernel_op_code << 16 | error_index` scheme and are not
|
||||
specified as kernel runtime error codes.
|
||||
- Resolution: not addressed (needs spec clarification or implementation changes
|
||||
to either remove/relocate `pel.bytes.params`, suppress diagnostics for kernel
|
||||
runtime failures, and/or treat internal/OOM as out-of-model rather than
|
||||
kernel runtime errors).
|
||||
- Tests: not run.
|
||||
|
|
|
|||
|
|
@ -249,6 +249,7 @@ enum {
|
|||
AMDUAT_PEL_DAG_DIAG_CYCLE = 0x00010008u,
|
||||
AMDUAT_PEL_DAG_DIAG_ROOT_OUTPUT_INDEX = 0x00010009u,
|
||||
AMDUAT_PEL_DAG_DIAG_INVALID_INPUT_INDEX = 0x00020001u,
|
||||
AMDUAT_PEL_DAG_DIAG_MISSING_PARAMS = 0x00020002u,
|
||||
AMDUAT_PEL_DAG_DIAG_OUTPUT_INDEX = 0x0001000au,
|
||||
AMDUAT_PEL_DAG_DIAG_RUNTIME_FAILED = 0x00030001u,
|
||||
AMDUAT_PEL_DAG_DIAG_NODE_RUNTIME_FAILED = 0x00030002u
|
||||
|
|
@ -1030,6 +1031,17 @@ static bool amduat_pel_program_dag_exec_internal(
|
|||
size_t j;
|
||||
uint32_t status_code = 0;
|
||||
|
||||
if (prepared.ops[node_index]->kind == AMDUAT_PEL_KERNEL_OP_PARAMS &&
|
||||
params == NULL) {
|
||||
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS,
|
||||
AMDUAT_PEL_EXEC_ERROR_INPUTS, 3);
|
||||
amduat_diag_setf(out_result,
|
||||
AMDUAT_PEL_DAG_DIAG_MISSING_PARAMS,
|
||||
"invalid inputs: missing params artifact");
|
||||
free(resolved_inputs);
|
||||
goto finish;
|
||||
}
|
||||
|
||||
for (j = 0; j < node->inputs_len; ++j) {
|
||||
const amduat_pel_dag_input_t *input = &node->inputs[j];
|
||||
if (input->kind == AMDUAT_PEL_DAG_INPUT_EXTERNAL) {
|
||||
|
|
|
|||
|
|
@ -1066,6 +1066,90 @@ cleanup_store:
|
|||
return exit_code;
|
||||
}
|
||||
|
||||
static int test_surf_missing_params(void) {
|
||||
stub_store_t stub;
|
||||
amduat_asl_store_t store;
|
||||
amduat_asl_store_ops_t ops;
|
||||
amduat_asl_store_config_t cfg;
|
||||
amduat_artifact_t program_artifact;
|
||||
amduat_reference_t program_ref;
|
||||
amduat_reference_t *output_refs = NULL;
|
||||
size_t output_refs_len = 0;
|
||||
amduat_reference_t result_ref;
|
||||
amduat_artifact_t result_artifact;
|
||||
amduat_pel_surface_execution_result_t decoded;
|
||||
int exit_code = 1;
|
||||
|
||||
cfg.encoding_profile_id = AMDUAT_ENC_ASL1_CORE_V1;
|
||||
cfg.hash_id = AMDUAT_HASH_ASL1_ID_SHA256;
|
||||
stub_store_init(&stub);
|
||||
stub.config = cfg;
|
||||
amduat_asl_store_ops_init(&ops);
|
||||
ops.put = stub_store_put;
|
||||
ops.get = stub_store_get;
|
||||
amduat_asl_store_init(&store, cfg, ops, &stub);
|
||||
program_ref = amduat_reference(0, amduat_octets(NULL, 0));
|
||||
result_ref = amduat_reference(0, amduat_octets(NULL, 0));
|
||||
|
||||
if (!build_params_program_artifact(&program_artifact)) {
|
||||
fprintf(stderr, "build params program failed\n");
|
||||
goto cleanup_store;
|
||||
}
|
||||
if (stub_store_put(&stub, program_artifact, &program_ref) !=
|
||||
AMDUAT_ASL_STORE_OK) {
|
||||
fprintf(stderr, "program put failed\n");
|
||||
free((void *)program_artifact.bytes.data);
|
||||
goto cleanup_store;
|
||||
}
|
||||
free((void *)program_artifact.bytes.data);
|
||||
|
||||
if (!amduat_pel_surf_run(&store, amduat_pel_program_dag_scheme_ref(),
|
||||
program_ref, NULL, 0, false,
|
||||
amduat_reference(0, amduat_octets(NULL, 0)),
|
||||
&output_refs, &output_refs_len, &result_ref)) {
|
||||
fprintf(stderr, "surf run failed\n");
|
||||
goto cleanup_refs;
|
||||
}
|
||||
|
||||
if (output_refs_len != 0) {
|
||||
fprintf(stderr, "unexpected output refs\n");
|
||||
goto cleanup_refs;
|
||||
}
|
||||
|
||||
if (stub_store_get(&stub, result_ref, &result_artifact) !=
|
||||
AMDUAT_ASL_STORE_OK) {
|
||||
fprintf(stderr, "result get failed\n");
|
||||
goto cleanup_refs;
|
||||
}
|
||||
if (!amduat_enc_pel1_result_decode_v1(result_artifact.bytes, &decoded)) {
|
||||
artifact_free(&result_artifact);
|
||||
fprintf(stderr, "result decode failed\n");
|
||||
goto cleanup_refs;
|
||||
}
|
||||
artifact_free(&result_artifact);
|
||||
|
||||
if (decoded.core_result.status != AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS ||
|
||||
decoded.core_result.summary.kind != AMDUAT_PEL_EXEC_ERROR_INPUTS ||
|
||||
decoded.core_result.summary.status_code != 3 ||
|
||||
decoded.has_store_failure ||
|
||||
decoded.has_params_ref) {
|
||||
fprintf(stderr, "missing params mapping mismatch\n");
|
||||
goto cleanup_decoded;
|
||||
}
|
||||
|
||||
exit_code = 0;
|
||||
|
||||
cleanup_decoded:
|
||||
amduat_enc_pel1_result_free(&decoded);
|
||||
cleanup_refs:
|
||||
amduat_pel_surf_free_refs(output_refs, output_refs_len);
|
||||
amduat_pel_surf_free_ref(&result_ref);
|
||||
amduat_pel_surf_free_ref(&program_ref);
|
||||
cleanup_store:
|
||||
stub_store_free(&stub);
|
||||
return exit_code;
|
||||
}
|
||||
|
||||
int main(void) {
|
||||
if (test_surf_success() != 0) {
|
||||
return 1;
|
||||
|
|
@ -1085,5 +1169,8 @@ int main(void) {
|
|||
if (test_surf_params_pass_through() != 0) {
|
||||
return 1;
|
||||
}
|
||||
if (test_surf_missing_params() != 0) {
|
||||
return 1;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2,9 +2,9 @@
|
|||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.1.1
|
||||
Version: 0.1.3
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Last Updated: 2025-12-22
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [registry, binary-minimalism]
|
||||
|
||||
|
|
@ -17,7 +17,7 @@ Tags: [registry, binary-minimalism]
|
|||
|
||||
* `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.1` — kernel operation semantics
|
||||
* `OPREG/PEL1-KERNEL v0.1.3` — kernel operation semantics
|
||||
|
||||
**Integrates with (informative):**
|
||||
|
||||
|
|
@ -51,6 +51,7 @@ public domain under CC0 1.0.
|
|||
* `pel.bytes.slice/1`
|
||||
* `pel.bytes.const/1`
|
||||
* `pel.bytes.hash.asl1/1`
|
||||
* `pel.bytes.params/1`
|
||||
|
||||
It specifies, for each operation:
|
||||
|
||||
|
|
@ -188,6 +189,9 @@ 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
|
||||
|
|
@ -211,11 +215,12 @@ This specification does **not** change these logical types; it only provides the
|
|||
|
||||
---
|
||||
|
||||
## 3. Unit Params Encoding (`pel.bytes.concat`)
|
||||
## 3. Unit Params Encoding (`pel.bytes.concat`, `pel.bytes.params`)
|
||||
|
||||
Applies to:
|
||||
|
||||
* `pel.bytes.concat/1`
|
||||
* `pel.bytes.params/1`
|
||||
|
||||
### 3.1 Logical type
|
||||
|
||||
|
|
@ -257,7 +262,7 @@ Algorithm:
|
|||
|
||||
### 3.4 Conformance rule
|
||||
|
||||
For `pel.bytes.concat/1`:
|
||||
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`.
|
||||
|
|
@ -638,6 +643,15 @@ An implementation is **OPREG/PEL1-KERNEL-PARAMS/1–conformant** if and only if:
|
|||
|
||||
## 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`:
|
||||
|
|
@ -671,4 +685,6 @@ An implementation is **OPREG/PEL1-KERNEL-PARAMS/1–conformant** if and only if:
|
|||
|
||||
## 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.
|
||||
|
|
|
|||
|
|
@ -2,9 +2,9 @@
|
|||
|
||||
Status: Approved
|
||||
Owner: Niklas Rydberg
|
||||
Version: 0.1.1
|
||||
Version: 0.1.3
|
||||
SoT: Yes
|
||||
Last Updated: 2025-11-16
|
||||
Last Updated: 2025-12-22
|
||||
Linked Phase Pack: N/A
|
||||
Tags: [registry, execution]
|
||||
|
||||
|
|
@ -282,7 +282,7 @@ All kernel operations in this registry share these properties:
|
|||
|
||||
## 3. Kernel Operation Index
|
||||
|
||||
We define four kernel operations:
|
||||
We define five kernel operations:
|
||||
|
||||
| Kernel Op Code | OperationId.name | version | Summary |
|
||||
| -------------: | ----------------------- | :------ | --------------------------------------- |
|
||||
|
|
@ -290,6 +290,7 @@ We define four kernel operations:
|
|||
| `0x0002` | `"pel.bytes.slice"` | `1` | Take a byte slice of one artifact |
|
||||
| `0x0003` | `"pel.bytes.const"` | `1` | Produce a constant artifact from params |
|
||||
| `0x0004` | `"pel.bytes.hash.asl1"` | `1` | Hash an artifact’s bytes with ASL1 |
|
||||
| `0x0005` | `"pel.bytes.params"` | `1` | Return the global params artifact |
|
||||
|
||||
All operation names are case-sensitive UTF-8 strings.
|
||||
|
||||
|
|
@ -650,13 +651,77 @@ All failures (unsupported `hash_id`, bad Params, wrong arity) are static and mus
|
|||
|
||||
---
|
||||
|
||||
### 4.5 `pel.bytes.params` v1 (code 0x0005)
|
||||
|
||||
**OperationId**
|
||||
|
||||
```text
|
||||
name = "pel.bytes.params"
|
||||
version = 1
|
||||
kernel_op_code = 0x0005
|
||||
```
|
||||
|
||||
**Intent**
|
||||
|
||||
Return the scheme-level global `params` Artifact supplied to `Exec_DAG`.
|
||||
|
||||
#### 4.5.1 Params: `Unit`
|
||||
|
||||
Params: **none** (`Unit`).
|
||||
|
||||
Param decoding failures MUST be treated as `INVALID_PROGRAM`.
|
||||
|
||||
#### 4.5.2 Arity
|
||||
|
||||
* `min_inputs = 0`
|
||||
* `max_inputs = 0`
|
||||
|
||||
Any non-empty `inputs` list is a static error (`INVALID_PROGRAM`).
|
||||
|
||||
#### 4.5.3 Semantics
|
||||
|
||||
Given:
|
||||
|
||||
```text
|
||||
inputs = []
|
||||
params = optional Artifact
|
||||
```
|
||||
|
||||
If `params` is present:
|
||||
|
||||
* Output list is a single Artifact `C`:
|
||||
|
||||
```text
|
||||
C.bytes = params.bytes
|
||||
C.type_tag = params.type_tag
|
||||
```
|
||||
|
||||
If `params` is absent:
|
||||
|
||||
* `Exec_DAG` MUST treat this as **missing inputs** and return:
|
||||
|
||||
```text
|
||||
status = INVALID_INPUTS
|
||||
summary.kind = INPUTS
|
||||
summary.status_code = 3
|
||||
```
|
||||
|
||||
* No outputs are produced.
|
||||
|
||||
#### 4.5.4 Runtime error codes
|
||||
|
||||
*None.*
|
||||
All failures are static (bad Params encoding, wrong arity).
|
||||
|
||||
---
|
||||
|
||||
## 5. Conformance
|
||||
|
||||
An engine is **OPREG/PEL1-KERNEL–conformant** if and only if:
|
||||
|
||||
1. **Operation availability**
|
||||
|
||||
* It exposes the four operations defined in §3 with exactly the specified `OperationId { name, version }`.
|
||||
* It exposes the five operations defined in §3 with exactly the specified `OperationId { name, version }`.
|
||||
|
||||
2. **Arity and Params**
|
||||
|
||||
|
|
@ -668,6 +733,8 @@ An engine is **OPREG/PEL1-KERNEL–conformant** if and only if:
|
|||
* invalid or undecodable Params
|
||||
|
||||
as `INVALID_PROGRAM` per `PEL/PROGRAM-DAG/1` (i.e. `Exec_DAG` produces `status = INVALID_PROGRAM`, `summary.status_code = 2`).
|
||||
* For `pel.bytes.params/1`, if the scheme-level `params` Artifact is absent,
|
||||
`Exec_DAG` MUST return `INVALID_INPUTS` (`summary.status_code = 3`).
|
||||
|
||||
3. **Runtime semantics**
|
||||
|
||||
|
|
@ -705,6 +772,16 @@ An engine is **OPREG/PEL1-KERNEL–conformant** if and only if:
|
|||
|
||||
## 6. Change Log (informative)
|
||||
|
||||
**v0.1.3 (2025-12-22)**
|
||||
|
||||
* `pel.bytes.params/1` now requires the global `params` Artifact; missing
|
||||
params MUST yield `INVALID_INPUTS` rather than an empty output.
|
||||
|
||||
**v0.1.2 (2025-12-22)**
|
||||
|
||||
* Added `pel.bytes.params/1` (code `0x0005`) to return the global `params` Artifact.
|
||||
* Defined the empty-params behavior (`params` absent ⇒ empty bytes, no type tag).
|
||||
|
||||
**v0.1.1 (2025-11-15)**
|
||||
|
||||
* Removed `pel.bytes.clone/1` from the kernel operation index.
|
||||
|
|
@ -738,4 +815,6 @@ An engine is **OPREG/PEL1-KERNEL–conformant** if and only if:
|
|||
|
||||
## Document History
|
||||
|
||||
* **0.1.3 (2025-12-22):** Clarified `pel.bytes.params/1` missing-params handling.
|
||||
* **0.1.2 (2025-12-22):** Added `pel.bytes.params/1` to the kernel registry.
|
||||
* **0.1.1 (2025-11-16):** Registered as Tier-1 spec and aligned to the Amduat 2.0 substrate baseline.
|
||||
|
|
|
|||
Loading…
Reference in a new issue