From a932363ad03280174dac3f96f1d1f7646caa33d9 Mon Sep 17 00:00:00 2001 From: Carl Niklas Rydberg Date: Mon, 22 Dec 2025 12:17:40 +0100 Subject: [PATCH] pel: require params for pel.bytes.params and add test --- AUDITS.md | 30 ++++++++- src/pel_stack/program_dag/program_dag.c | 12 ++++ tests/pel/test_pel_surf_run.c | 87 +++++++++++++++++++++++++ tier1/opreg-pel1-kernel-params-1.md | 26 ++++++-- tier1/opreg-pel1-kernel.md | 87 +++++++++++++++++++++++-- 5 files changed, 231 insertions(+), 11 deletions(-) diff --git a/AUDITS.md b/AUDITS.md index ab01bcb..3ee5eb1 100644 --- a/AUDITS.md +++ b/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. diff --git a/src/pel_stack/program_dag/program_dag.c b/src/pel_stack/program_dag/program_dag.c index c97b866..f51c786 100644 --- a/src/pel_stack/program_dag/program_dag.c +++ b/src/pel_stack/program_dag/program_dag.c @@ -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) { diff --git a/tests/pel/test_pel_surf_run.c b/tests/pel/test_pel_surf_run.c index e00229f..92d1027 100644 --- a/tests/pel/test_pel_surf_run.c +++ b/tests/pel/test_pel_surf_run.c @@ -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; } diff --git a/tier1/opreg-pel1-kernel-params-1.md b/tier1/opreg-pel1-kernel-params-1.md index 36e37b5..40d298b 100644 --- a/tier1/opreg-pel1-kernel-params-1.md +++ b/tier1/opreg-pel1-kernel-params-1.md @@ -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. diff --git a/tier1/opreg-pel1-kernel.md b/tier1/opreg-pel1-kernel.md index 4c0a3c6..93c6468 100644 --- a/tier1/opreg-pel1-kernel.md +++ b/tier1/opreg-pel1-kernel.md @@ -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.