Adjusted PEL core execution to treat allocation failures as out‑of‑model (return false without a core result) and made amduat_pel_exec_program_bytes return deterministic ExecutionResultValue for invalid program bytes or missing inputs, as required by PEL/1‑CORE totality. Updates are in program_dag.c and run.c.

This commit is contained in:
Carl Niklas Rydberg 2025-12-22 00:31:31 +01:00
parent 87c8bcc799
commit 503ad05061
2 changed files with 88 additions and 42 deletions

View file

@ -131,12 +131,16 @@ static int amduat_find_node_index(const amduat_pel_program_t *program,
} }
static bool amduat_build_node_order(const amduat_pel_program_t *program, static bool amduat_build_node_order(const amduat_pel_program_t *program,
size_t *out_order) { size_t *out_order,
bool *out_oom) {
size_t n; size_t n;
size_t *deps; size_t *deps;
bool *placed; bool *placed;
size_t i; size_t i;
if (out_oom != NULL) {
*out_oom = false;
}
n = program->nodes_len; n = program->nodes_len;
deps = NULL; deps = NULL;
placed = NULL; placed = NULL;
@ -148,6 +152,9 @@ static bool amduat_build_node_order(const amduat_pel_program_t *program,
deps = (size_t *)calloc(n, sizeof(*deps)); deps = (size_t *)calloc(n, sizeof(*deps));
placed = (bool *)calloc(n, sizeof(*placed)); placed = (bool *)calloc(n, sizeof(*placed));
if (deps == NULL || placed == NULL) { if (deps == NULL || placed == NULL) {
if (out_oom != NULL) {
*out_oom = true;
}
free(deps); free(deps);
free(placed); free(placed);
return false; return false;
@ -307,28 +314,36 @@ static bool amduat_copy_artifact(amduat_artifact_t *out,
return true; return true;
} }
static bool amduat_program_prepare(const amduat_pel_program_t *program, typedef enum {
amduat_pel_program_dag_prepared_t *prepared) { AMDUAT_PEL_PROGRAM_PREP_OK = 0,
AMDUAT_PEL_PROGRAM_PREP_INVALID = 1,
AMDUAT_PEL_PROGRAM_PREP_OOM = 2
} amduat_pel_program_prepare_result_t;
static amduat_pel_program_prepare_result_t amduat_program_prepare(
const amduat_pel_program_t *program,
amduat_pel_program_dag_prepared_t *prepared) {
size_t i; size_t i;
bool oom;
if (program == NULL || prepared == NULL) { if (program == NULL || prepared == NULL) {
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
amduat_prepared_reset(prepared); amduat_prepared_reset(prepared);
if (program->nodes_len > 0 && program->nodes == NULL) { if (program->nodes_len > 0 && program->nodes == NULL) {
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (program->roots_len > 0 && program->roots == NULL) { if (program->roots_len > 0 && program->roots == NULL) {
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (program->nodes_len == 0) { if (program->nodes_len == 0) {
if (program->roots_len != 0) { if (program->roots_len != 0) {
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
return true; return AMDUAT_PEL_PROGRAM_PREP_OK;
} }
prepared->order = (size_t *)malloc(program->nodes_len * prepared->order = (size_t *)malloc(program->nodes_len *
@ -341,7 +356,7 @@ static bool amduat_program_prepare(const amduat_pel_program_t *program,
if (prepared->order == NULL || prepared->ops == NULL || if (prepared->order == NULL || prepared->ops == NULL ||
prepared->params == NULL) { prepared->params == NULL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_OOM;
} }
for (i = 0; i < program->nodes_len; ++i) { for (i = 0; i < program->nodes_len; ++i) {
@ -350,43 +365,45 @@ static bool amduat_program_prepare(const amduat_pel_program_t *program,
if (node->op.name.len > 0 && node->op.name.data == NULL) { if (node->op.name.len > 0 && node->op.name.data == NULL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (!amduat_utf8_is_valid(node->op.name)) { if (!amduat_utf8_is_valid(node->op.name)) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (node->inputs_len > 0 && node->inputs == NULL) { if (node->inputs_len > 0 && node->inputs == NULL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (node->params.len > 0 && node->params.data == NULL) { if (node->params.len > 0 && node->params.data == NULL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
desc = amduat_pel_kernel_op_lookup(node->op.name, node->op.version); desc = amduat_pel_kernel_op_lookup(node->op.name, node->op.version);
if (desc == NULL) { if (desc == NULL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (node->inputs_len < desc->min_inputs || if (node->inputs_len < desc->min_inputs ||
node->inputs_len > desc->max_inputs) { node->inputs_len > desc->max_inputs) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (!amduat_pel_kernel_params_decode(desc, node->params, if (!amduat_pel_kernel_params_decode(desc, node->params,
&prepared->params[i])) { &prepared->params[i])) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
prepared->ops[i] = desc; prepared->ops[i] = desc;
} }
if (!amduat_build_node_order(program, prepared->order)) { oom = false;
if (!amduat_build_node_order(program, prepared->order, &oom)) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return oom ? AMDUAT_PEL_PROGRAM_PREP_OOM
: AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
for (i = 0; i < program->nodes_len; ++i) { for (i = 0; i < program->nodes_len; ++i) {
@ -399,16 +416,16 @@ static bool amduat_program_prepare(const amduat_pel_program_t *program,
input->value.node.node_id); input->value.node.node_id);
if (dep_index < 0) { if (dep_index < 0) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (input->value.node.output_index >= if (input->value.node.output_index >=
prepared->ops[dep_index]->outputs_len) { prepared->ops[dep_index]->outputs_len) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
} else if (input->kind != AMDUAT_PEL_DAG_INPUT_EXTERNAL) { } else if (input->kind != AMDUAT_PEL_DAG_INPUT_EXTERNAL) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
} }
} }
@ -417,26 +434,26 @@ static bool amduat_program_prepare(const amduat_pel_program_t *program,
int root_index = amduat_find_node_index(program, program->roots[i].node_id); int root_index = amduat_find_node_index(program, program->roots[i].node_id);
if (root_index < 0) { if (root_index < 0) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
if (program->roots[i].output_index >= if (program->roots[i].output_index >=
prepared->ops[root_index]->outputs_len) { prepared->ops[root_index]->outputs_len) {
amduat_prepared_free(prepared); amduat_prepared_free(prepared);
return false; return AMDUAT_PEL_PROGRAM_PREP_INVALID;
} }
} }
return true; return AMDUAT_PEL_PROGRAM_PREP_OK;
} }
bool amduat_pel_program_dag_validate(const amduat_pel_program_t *program) { bool amduat_pel_program_dag_validate(const amduat_pel_program_t *program) {
amduat_pel_program_dag_prepared_t prepared; amduat_pel_program_dag_prepared_t prepared;
bool ok; amduat_pel_program_prepare_result_t prep_result;
amduat_prepared_reset(&prepared); amduat_prepared_reset(&prepared);
ok = amduat_program_prepare(program, &prepared); prep_result = amduat_program_prepare(program, &prepared);
amduat_prepared_free(&prepared); amduat_prepared_free(&prepared);
return ok; return prep_result == AMDUAT_PEL_PROGRAM_PREP_OK;
} }
static bool amduat_pel_program_dag_exec_internal( static bool amduat_pel_program_dag_exec_internal(
@ -448,6 +465,7 @@ static bool amduat_pel_program_dag_exec_internal(
amduat_pel_execution_result_value_t *out_result, amduat_pel_execution_result_value_t *out_result,
amduat_pel_program_dag_trace_t *out_trace) { amduat_pel_program_dag_trace_t *out_trace) {
amduat_pel_program_dag_prepared_t prepared; amduat_pel_program_dag_prepared_t prepared;
amduat_pel_program_prepare_result_t prep_result;
amduat_pel_program_dag_node_result_t *node_results; amduat_pel_program_dag_node_result_t *node_results;
amduat_artifact_t *resolved_inputs; amduat_artifact_t *resolved_inputs;
size_t max_inputs; size_t max_inputs;
@ -467,7 +485,11 @@ static bool amduat_pel_program_dag_exec_internal(
} }
amduat_prepared_reset(&prepared); amduat_prepared_reset(&prepared);
if (!amduat_program_prepare(program, &prepared)) { prep_result = amduat_program_prepare(program, &prepared);
if (prep_result == AMDUAT_PEL_PROGRAM_PREP_OOM) {
return false;
}
if (prep_result != AMDUAT_PEL_PROGRAM_PREP_OK) {
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM, amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM,
AMDUAT_PEL_EXEC_ERROR_PROGRAM, 2); AMDUAT_PEL_EXEC_ERROR_PROGRAM, 2);
amduat_prepared_free(&prepared); amduat_prepared_free(&prepared);
@ -507,10 +529,8 @@ static bool amduat_pel_program_dag_exec_internal(
node_results = (amduat_pel_program_dag_node_result_t *)calloc( node_results = (amduat_pel_program_dag_node_result_t *)calloc(
program->nodes_len, sizeof(*node_results)); program->nodes_len, sizeof(*node_results));
if (node_results == NULL) { if (node_results == NULL) {
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED,
AMDUAT_PEL_EXEC_ERROR_RUNTIME, 1);
amduat_prepared_free(&prepared); amduat_prepared_free(&prepared);
return true; return false;
} }
for (i = 0; i < program->nodes_len; ++i) { for (i = 0; i < program->nodes_len; ++i) {
node_results[i].status = AMDUAT_PEL_NODE_TRACE_SKIPPED; node_results[i].status = AMDUAT_PEL_NODE_TRACE_SKIPPED;
@ -529,11 +549,9 @@ static bool amduat_pel_program_dag_exec_internal(
resolved_inputs = (amduat_artifact_t *)malloc( resolved_inputs = (amduat_artifact_t *)malloc(
max_inputs * sizeof(*resolved_inputs)); max_inputs * sizeof(*resolved_inputs));
if (resolved_inputs == NULL) { if (resolved_inputs == NULL) {
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED,
AMDUAT_PEL_EXEC_ERROR_RUNTIME, 1);
amduat_node_results_free(node_results, program->nodes_len); amduat_node_results_free(node_results, program->nodes_len);
amduat_prepared_free(&prepared); amduat_prepared_free(&prepared);
return true; return false;
} }
} }
@ -598,10 +616,8 @@ static bool amduat_pel_program_dag_exec_internal(
*out_outputs = (amduat_artifact_t *)calloc( *out_outputs = (amduat_artifact_t *)calloc(
program->roots_len, sizeof(**out_outputs)); program->roots_len, sizeof(**out_outputs));
if (*out_outputs == NULL) { if (*out_outputs == NULL) {
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED,
AMDUAT_PEL_EXEC_ERROR_RUNTIME, 1);
free(resolved_inputs); free(resolved_inputs);
goto finish; goto oom_finish;
} }
} }
@ -623,14 +639,12 @@ static bool amduat_pel_program_dag_exec_internal(
&(*out_outputs)[i], &(*out_outputs)[i],
&node_results[root_index] &node_results[root_index]
.outputs[program->roots[i].output_index])) { .outputs[program->roots[i].output_index])) {
amduat_set_result(out_result, AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED,
AMDUAT_PEL_EXEC_ERROR_RUNTIME, 1);
amduat_pel_program_dag_free_outputs(*out_outputs, amduat_pel_program_dag_free_outputs(*out_outputs,
program->roots_len); program->roots_len);
*out_outputs = NULL; *out_outputs = NULL;
*out_outputs_len = 0; *out_outputs_len = 0;
free(resolved_inputs); free(resolved_inputs);
goto finish; goto oom_finish;
} }
} }
@ -658,6 +672,23 @@ finish:
} }
amduat_prepared_free(&prepared); amduat_prepared_free(&prepared);
return true; return true;
oom_finish:
if (wants_trace) {
out_trace->any_node_executed = any_node_executed;
if (any_node_executed) {
amduat_node_results_free(node_results, program->nodes_len);
node_results = NULL;
} else {
amduat_node_results_free(node_results, program->nodes_len);
node_results = NULL;
}
} else {
amduat_node_results_free(node_results, program->nodes_len);
node_results = NULL;
}
amduat_prepared_free(&prepared);
return false;
} }
bool amduat_pel_program_dag_exec( bool amduat_pel_program_dag_exec(

View file

@ -4,6 +4,7 @@
#include "amduat/enc/pel1_result.h" #include "amduat/enc/pel1_result.h"
#include "amduat/enc/pel_program_dag.h" #include "amduat/enc/pel_program_dag.h"
#include "amduat/pel/program_dag.h" #include "amduat/pel/program_dag.h"
#include "amduat/pel/program_dag_desc.h"
#include <string.h> #include <string.h>
@ -60,7 +61,14 @@ bool amduat_pel_exec_program_bytes(amduat_octets_t program_bytes,
return false; return false;
} }
if (inputs_len != 0 && inputs == NULL) { if (inputs_len != 0 && inputs == NULL) {
return false; out_result->pel1_version = 1;
out_result->status = AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS;
out_result->scheme_ref = amduat_pel_program_dag_scheme_ref();
out_result->summary.kind = AMDUAT_PEL_EXEC_ERROR_INPUTS;
out_result->summary.status_code = 3;
out_result->diagnostics = NULL;
out_result->diagnostics_len = 0;
return true;
} }
*out_outputs = NULL; *out_outputs = NULL;
@ -69,7 +77,14 @@ bool amduat_pel_exec_program_bytes(amduat_octets_t program_bytes,
memset(&program, 0, sizeof(program)); memset(&program, 0, sizeof(program));
if (!amduat_enc_pel_program_dag_decode_v1(program_bytes, &program)) { if (!amduat_enc_pel_program_dag_decode_v1(program_bytes, &program)) {
return false; out_result->pel1_version = 1;
out_result->status = AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM;
out_result->scheme_ref = amduat_pel_program_dag_scheme_ref();
out_result->summary.kind = AMDUAT_PEL_EXEC_ERROR_PROGRAM;
out_result->summary.status_code = 2;
out_result->diagnostics = NULL;
out_result->diagnostics_len = 0;
return true;
} }
ok = amduat_pel_program_dag_exec(&program, ok = amduat_pel_program_dag_exec(&program,