Enforce PEL1 result invariants and add regression test

CMakeLists.txt

@@ -233,6 +233,18 @@ target_link_libraries(amduat_test_pel1_result
 )
 add_test(NAME pel1_result COMMAND amduat_test_pel1_result)
 
+add_executable(amduat_test_pel1_result_invariants
+  tests/enc/test_pel1_result_invariants.c)
+target_include_directories(amduat_test_pel1_result_invariants
+  PRIVATE ${AMDUAT_INTERNAL_DIR}
+  PRIVATE ${AMDUAT_INCLUDE_DIR}
+)
+target_link_libraries(amduat_test_pel1_result_invariants
+  PRIVATE amduat_enc amduat_hash_asl1 amduat_asl amduat_util
+)
+add_test(NAME pel1_result_invariants
+  COMMAND amduat_test_pel1_result_invariants)
+
 add_executable(amduat_test_tgk1_edge tests/enc/test_tgk1_edge.c)
 target_include_directories(amduat_test_tgk1_edge
   PRIVATE ${AMDUAT_INTERNAL_DIR}

src/near_core/enc/pel1_result.c

@@ -66,6 +66,55 @@ static bool amduat_add_size(size_t *acc, size_t add) {
   return true;
 }
 
+static bool amduat_execution_summary_valid(
+    amduat_pel_execution_status_t status,
+    amduat_pel_execution_error_summary_t summary) {
+  switch (status) {
+    case AMDUAT_PEL_EXEC_STATUS_OK:
+      return summary.kind == AMDUAT_PEL_EXEC_ERROR_NONE &&
+             summary.status_code == 0;
+    case AMDUAT_PEL_EXEC_STATUS_SCHEME_UNSUPPORTED:
+      return summary.kind == AMDUAT_PEL_EXEC_ERROR_SCHEME;
+    case AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM:
+      return summary.kind == AMDUAT_PEL_EXEC_ERROR_PROGRAM;
+    case AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS:
+      return summary.kind == AMDUAT_PEL_EXEC_ERROR_INPUTS;
+    case AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED:
+      return summary.kind == AMDUAT_PEL_EXEC_ERROR_RUNTIME &&
+             summary.status_code != 0;
+    default:
+      return false;
+  }
+}
+
+static bool amduat_execution_status_valid(
+    amduat_pel_execution_status_t status) {
+  switch (status) {
+    case AMDUAT_PEL_EXEC_STATUS_OK:
+    case AMDUAT_PEL_EXEC_STATUS_SCHEME_UNSUPPORTED:
+    case AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM:
+    case AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS:
+    case AMDUAT_PEL_EXEC_STATUS_RUNTIME_FAILED:
+      return true;
+    default:
+      return false;
+  }
+}
+
+static bool amduat_execution_error_kind_valid(
+    amduat_pel_execution_error_kind_t kind) {
+  switch (kind) {
+    case AMDUAT_PEL_EXEC_ERROR_NONE:
+    case AMDUAT_PEL_EXEC_ERROR_SCHEME:
+    case AMDUAT_PEL_EXEC_ERROR_PROGRAM:
+    case AMDUAT_PEL_EXEC_ERROR_INPUTS:
+    case AMDUAT_PEL_EXEC_ERROR_RUNTIME:
+      return true;
+    default:
+      return false;
+  }
+}
+
 static bool amduat_reference_bytes_len(amduat_reference_t ref, size_t *out_len) {
   const amduat_hash_asl1_desc_t *desc;
 
@@ -259,6 +308,9 @@ static bool amduat_read_execution_result_value(
   if (!amduat_read_u8(cur, &out_value->status)) {
     return false;
   }
+  if (!amduat_execution_status_valid(out_value->status)) {
+    return false;
+  }
   if (!amduat_read_encoded_ref(cur, &out_value->scheme_ref)) {
     return false;
   }
@@ -266,6 +318,9 @@ static bool amduat_read_execution_result_value(
       !amduat_read_u32(cur, &out_value->summary.status_code)) {
     return false;
   }
+  if (!amduat_execution_error_kind_valid(out_value->summary.kind)) {
+    return false;
+  }
   if (!amduat_read_u32(cur, &diag_count)) {
     return false;
   }
@@ -369,6 +424,10 @@ bool amduat_enc_pel1_result_encode_v1(
                            result->core_result.scheme_ref)) {
     return false;
   }
+  if (!amduat_execution_summary_valid(result->core_result.status,
+                                      result->core_result.summary)) {
+    return false;
+  }
   if (result->input_refs_len > UINT32_MAX ||
       result->output_refs_len > UINT32_MAX) {
     return false;
@@ -433,6 +492,19 @@ bool amduat_enc_pel1_result_encode_v1(
     return false;
   }
   if (result->has_store_failure) {
+    if (result->store_failure.phase == AMDUAT_PEL_STORE_FAILURE_PROGRAM) {
+      if (result->core_result.status != AMDUAT_PEL_EXEC_STATUS_INVALID_PROGRAM ||
+          result->core_result.summary.kind != AMDUAT_PEL_EXEC_ERROR_PROGRAM) {
+        return false;
+      }
+    } else if (result->store_failure.phase == AMDUAT_PEL_STORE_FAILURE_INPUT) {
+      if (result->core_result.status != AMDUAT_PEL_EXEC_STATUS_INVALID_INPUTS ||
+          result->core_result.summary.kind != AMDUAT_PEL_EXEC_ERROR_INPUTS) {
+        return false;
+      }
+    } else {
+      return false;
+    }
     size_t enc_len;
     if (!amduat_encoded_ref_len(result->store_failure.failing_ref, &enc_len)) {
       return false;

tests/enc/test_pel1_result_invariants.c

@@ -0,0 +1,162 @@
+#include "amduat/enc/pel1_result.h"
+
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+static void fill_digest(uint8_t *out, uint8_t value) {
+  memset(out, value, 32);
+}
+
+static amduat_reference_t make_ref(uint8_t value, uint8_t *storage) {
+  fill_digest(storage, value);
+  return amduat_reference(0x0001, amduat_octets(storage, 32));
+}
+
+static void init_base_result(amduat_pel_surface_execution_result_t *result,
+                             uint8_t *scheme_digest,
+                             uint8_t *program_digest) {
+  memset(result, 0, sizeof(*result));
+  result->pel1_version = 1;
+  result->scheme_ref = make_ref(0x01, scheme_digest);
+  result->program_ref = make_ref(0x02, program_digest);
+  result->input_refs = NULL;
+  result->input_refs_len = 0;
+  result->output_refs = NULL;
+  result->output_refs_len = 0;
+  result->has_params_ref = false;
+  result->has_store_failure = false;
+  result->has_trace_ref = false;
+
+  result->core_result.pel1_version = 1;
+  result->core_result.status = AMDUAT_PEL_EXEC_STATUS_OK;
+  result->core_result.scheme_ref = result->scheme_ref;
+  result->core_result.summary.kind = AMDUAT_PEL_EXEC_ERROR_NONE;
+  result->core_result.summary.status_code = 0;
+  result->core_result.diagnostics = NULL;
+  result->core_result.diagnostics_len = 0;
+}
+
+static int test_encode_status_invariant(void) {
+  amduat_pel_surface_execution_result_t result;
+  amduat_octets_t encoded = amduat_octets(NULL, 0);
+  uint8_t s[32], p[32];
+
+  init_base_result(&result, s, p);
+  result.core_result.summary.status_code = 7;
+
+  if (amduat_enc_pel1_result_encode_v1(&result, &encoded)) {
+    fprintf(stderr, "expected encode failure for OK status with nonzero code\n");
+    amduat_octets_free(&encoded);
+    return 1;
+  }
+
+  return 0;
+}
+
+static int test_encode_store_failure_invariant(void) {
+  amduat_pel_surface_execution_result_t result;
+  amduat_octets_t encoded = amduat_octets(NULL, 0);
+  uint8_t s[32], p[32], f[32];
+
+  init_base_result(&result, s, p);
+  result.has_store_failure = true;
+  result.store_failure.phase = AMDUAT_PEL_STORE_FAILURE_PROGRAM;
+  result.store_failure.error_code = AMDUAT_PEL_STORE_ERROR_NOT_FOUND;
+  result.store_failure.failing_ref = make_ref(0x03, f);
+
+  if (amduat_enc_pel1_result_encode_v1(&result, &encoded)) {
+    fprintf(stderr, "expected encode failure for store_failure mismatch\n");
+    amduat_octets_free(&encoded);
+    return 1;
+  }
+
+  return 0;
+}
+
+static bool mutate_and_decode(amduat_octets_t encoded,
+                              size_t offset,
+                              uint8_t value) {
+  amduat_pel_surface_execution_result_t decoded;
+  bool ok;
+
+  if (offset >= encoded.len) {
+    return false;
+  }
+  ((uint8_t *)encoded.data)[offset] = value;
+  ok = amduat_enc_pel1_result_decode_v1(encoded, &decoded);
+  if (ok) {
+    amduat_enc_pel1_result_free(&decoded);
+  }
+  return ok;
+}
+
+static int test_decode_invalid_status_kind(void) {
+  amduat_pel_surface_execution_result_t result;
+  amduat_octets_t encoded = amduat_octets(NULL, 0);
+  uint8_t *original = NULL;
+  uint8_t s[32], p[32];
+  size_t encoded_ref_len = 4 + 2 + 32;
+  size_t offset = 0;
+  size_t status_offset;
+  size_t kind_offset;
+
+  init_base_result(&result, s, p);
+  if (!amduat_enc_pel1_result_encode_v1(&result, &encoded)) {
+    fprintf(stderr, "encode failed\n");
+    return 1;
+  }
+  if (encoded.len != 0) {
+    original = (uint8_t *)malloc(encoded.len);
+    if (original == NULL) {
+      fprintf(stderr, "alloc failed\n");
+      amduat_octets_free(&encoded);
+      return 1;
+    }
+    memcpy(original, encoded.data, encoded.len);
+  }
+
+  offset += 2;
+  offset += encoded_ref_len;
+  offset += encoded_ref_len;
+  offset += 4;
+  offset += 4;
+  offset += 1;
+  offset += 1;
+  offset += 1;
+  offset += 2;
+  status_offset = offset;
+  kind_offset = status_offset + 1 + encoded_ref_len;
+
+  if (mutate_and_decode(encoded, status_offset, 0xffu)) {
+    fprintf(stderr, "expected decode failure for invalid status\n");
+    goto cleanup;
+  }
+  if (original != NULL) {
+    memcpy((uint8_t *)encoded.data, original, encoded.len);
+  }
+  if (mutate_and_decode(encoded, kind_offset, 0xffu)) {
+    fprintf(stderr, "expected decode failure for invalid summary kind\n");
+    goto cleanup;
+  }
+
+cleanup:
+  free(original);
+  amduat_octets_free(&encoded);
+  return 0;
+}
+
+int main(void) {
+  if (test_encode_status_invariant() != 0) {
+    return 1;
+  }
+  if (test_encode_store_failure_invariant() != 0) {
+    return 1;
+  }
+  if (test_decode_invalid_status_kind() != 0) {
+    return 1;
+  }
+  return 0;
+}