Something

CMakeLists.txt

@@ -79,6 +79,8 @@ set(AMDUAT_ENC_SRCS
   src/near_core/enc/asl1_core.c
   src/near_core/enc/asl1_core_codec.c
   src/near_core/asl/ref_derive.c
+  src/near_core/enc/fer1_receipt.c
+  src/near_core/fer/receipt.c
   src/near_core/enc/pel_program_dag.c
   src/near_core/enc/pel_program_dag_desc.c
   src/near_core/enc/pel_trace_dag.c
@@ -255,6 +257,16 @@ target_link_libraries(amduat_test_tgk1_edge
 )
 add_test(NAME tgk1_edge COMMAND amduat_test_tgk1_edge)
 
+add_executable(amduat_test_fer1_receipt tests/enc/test_fer1_receipt.c)
+target_include_directories(amduat_test_fer1_receipt
+  PRIVATE ${AMDUAT_INTERNAL_DIR}
+  PRIVATE ${AMDUAT_INCLUDE_DIR}
+)
+target_link_libraries(amduat_test_fer1_receipt
+  PRIVATE amduat_enc amduat_hash_asl1 amduat_asl amduat_util
+)
+add_test(NAME fer1_receipt COMMAND amduat_test_fer1_receipt)
+
 add_executable(amduat_test_tgk_store_mem tests/tgk/test_tgk_store_mem.c)
 target_include_directories(amduat_test_tgk_store_mem
   PRIVATE ${AMDUAT_INTERNAL_DIR}

include/amduat/enc/fer1_receipt.h

@@ -0,0 +1,53 @@
+#ifndef AMDUAT_ENC_FER1_RECEIPT_H
+#define AMDUAT_ENC_FER1_RECEIPT_H
+
+#include "amduat/asl/core.h"
+
+#include <stdbool.h>
+#include <stddef.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+enum { FER1_RECEIPT_ENC_V1 = 0x0301u };
+
+enum { TYPE_TAG_FER1_RECEIPT_1 = 0x00000301u };
+enum { AMDUAT_TYPE_TAG_FER1_RECEIPT_1 = TYPE_TAG_FER1_RECEIPT_1 };
+
+typedef struct {
+  amduat_reference_t executor_ref;
+  amduat_reference_t output_ref;
+  bool has_sbom_ref;
+  amduat_reference_t sbom_ref;
+  amduat_octets_t parity_digest;
+} amduat_fer1_parity_entry_t;
+
+typedef struct {
+  uint16_t fer1_version;
+  amduat_reference_t function_ref;
+  amduat_reference_t input_manifest_ref;
+  amduat_reference_t environment_ref;
+  amduat_octets_t evaluator_id;
+  amduat_reference_t output_ref;
+  amduat_reference_t *executor_refs;
+  size_t executor_refs_len;
+  amduat_fer1_parity_entry_t *parity;
+  size_t parity_len;
+  uint64_t started_at;
+  uint64_t completed_at;
+} amduat_fer1_receipt_t;
+
+bool amduat_enc_fer1_receipt_encode_v1(
+    const amduat_fer1_receipt_t *receipt,
+    amduat_octets_t *out_bytes);
+bool amduat_enc_fer1_receipt_decode_v1(
+    amduat_octets_t bytes,
+    amduat_fer1_receipt_t *out_receipt);
+void amduat_enc_fer1_receipt_free(amduat_fer1_receipt_t *receipt);
+
+#ifdef __cplusplus
+} /* extern "C" */
+#endif
+
+#endif /* AMDUAT_ENC_FER1_RECEIPT_H */

include/amduat/fer/receipt.h

@@ -0,0 +1,31 @@
+#ifndef AMDUAT_FER_RECEIPT_H
+#define AMDUAT_FER_RECEIPT_H
+
+#include "amduat/asl/core.h"
+#include "amduat/pel/surf.h"
+
+#include <stdbool.h>
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+bool amduat_fer1_receipt_from_pel_result(
+    const amduat_pel_surface_execution_result_t *pel_result,
+    amduat_reference_t input_manifest_ref,
+    amduat_reference_t environment_ref,
+    amduat_octets_t evaluator_id,
+    amduat_reference_t executor_ref,
+    bool has_sbom_ref,
+    amduat_reference_t sbom_ref,
+    amduat_octets_t parity_digest,
+    uint64_t started_at,
+    uint64_t completed_at,
+    amduat_artifact_t *out_artifact);
+
+#ifdef __cplusplus
+} /* extern "C" */
+#endif
+
+#endif /* AMDUAT_FER_RECEIPT_H */

include/amduat/pel/opreg_kernel.h

@@ -16,20 +16,26 @@ extern "C" {
 #define AMDUAT_PEL_KERNEL_OP_CONST_NAME "pel.bytes.const"
 #define AMDUAT_PEL_KERNEL_OP_HASH_ASL1_NAME "pel.bytes.hash.asl1"
 #define AMDUAT_PEL_KERNEL_OP_PARAMS_NAME "pel.bytes.params"
+#define AMDUAT_PEL_KERNEL_OP_FORMAT_ENCODE_NAME "pel.format.encode"
 
 enum {
   AMDUAT_PEL_KERNEL_OP_CODE_CONCAT = 0x0001u,
   AMDUAT_PEL_KERNEL_OP_CODE_SLICE = 0x0002u,
   AMDUAT_PEL_KERNEL_OP_CODE_CONST = 0x0003u,
   AMDUAT_PEL_KERNEL_OP_CODE_HASH_ASL1 = 0x0004u,
-  AMDUAT_PEL_KERNEL_OP_CODE_PARAMS = 0x0005u
+  AMDUAT_PEL_KERNEL_OP_CODE_PARAMS = 0x0005u,
+  AMDUAT_PEL_KERNEL_OP_CODE_FORMAT_ENCODE = 0x0006u
 };
 
 enum {
   AMDUAT_PEL_KERNEL_STATUS_OOM = 0x00000001u,
   AMDUAT_PEL_KERNEL_STATUS_INTERNAL = 0x00000002u,
   AMDUAT_PEL_KERNEL_STATUS_CONCAT_TYPE_TAG_MISMATCH = 0x00010001u,
-  AMDUAT_PEL_KERNEL_STATUS_SLICE_RANGE_OUT_OF_BOUNDS = 0x00020001u
+  AMDUAT_PEL_KERNEL_STATUS_SLICE_RANGE_OUT_OF_BOUNDS = 0x00020001u,
+  AMDUAT_PEL_KERNEL_STATUS_FORMAT_SCHEMA_INVALID = 0x00030001u,
+  AMDUAT_PEL_KERNEL_STATUS_FORMAT_REGISTRY_INVALID = 0x00030002u,
+  AMDUAT_PEL_KERNEL_STATUS_FORMAT_MISSING_FIELD = 0x00030003u,
+  AMDUAT_PEL_KERNEL_STATUS_FORMAT_TYPE_UNSUPPORTED = 0x00030004u
 };
 
 typedef enum {
@@ -37,7 +43,8 @@ typedef enum {
   AMDUAT_PEL_KERNEL_OP_SLICE = 2,
   AMDUAT_PEL_KERNEL_OP_CONST = 3,
   AMDUAT_PEL_KERNEL_OP_HASH_ASL1 = 4,
-  AMDUAT_PEL_KERNEL_OP_PARAMS = 5
+  AMDUAT_PEL_KERNEL_OP_PARAMS = 5,
+  AMDUAT_PEL_KERNEL_OP_FORMAT_ENCODE = 6
 } amduat_pel_kernel_op_kind_t;
 
 typedef struct {

registry/type-tag.jsonl

@@ -3,3 +3,4 @@
 {"registry":"TYPE/ASL1","tag_id":"0x00000102","handle":"amduat.type.asl1.tag.00000102@1","name":"TYPE_TAG_PEL_TRACE_DAG_1","status":"mandatory","spec_ref":"ENC/PEL-TRACE-DAG/1 v0.1.0","notes":"Canonical TypeTag for PEL/TRACE-DAG/1 Trace Artifacts.","descriptor_sha256":"e044e3d9423442c51d3a2008a090aeca5575ca5ba30293965dd40c6baa67b3d2"}
 {"registry":"TYPE/ASL1","tag_id":"0x00000103","handle":"amduat.type.asl1.tag.00000103@1","name":"TYPE_TAG_PEL1_RESULT_1","status":"mandatory","spec_ref":"ENC/PEL1-RESULT/1 v0.3.0","notes":"Canonical TypeTag for PEL/1 ExecutionResult Artifacts.","descriptor_sha256":"0e90731d9fbb4cddf4a1fae055faad66a19db33eab199e9a53db716ca07cef83"}
 {"registry":"TYPE/ASL1","tag_id":"0x00000201","handle":"amduat.type.asl1.tag.00000201@1","name":"TYPE_TAG_TGK1_EDGE_V1","status":"mandatory","spec_ref":"ENC/TGK1-EDGE/1 v0.1.0","notes":"Canonical TypeTag for TGK1 EdgeArtifacts encoded with ENC/TGK1-EDGE/1.","descriptor_sha256":"5a6c0733433544923a98317e1c3bebfc3e0fb3f9e8ec1975be3d936b417f5990"}
+{"registry":"TYPE/ASL1","tag_id":"0x00000301","handle":"amduat.type.asl1.tag.00000301@1","name":"TYPE_TAG_FER1_RECEIPT_1","status":"mandatory","spec_ref":"ENC/FER1-RECEIPT/1 v0.1.0","notes":"Canonical TypeTag for FER/1 Receipt Artifacts encoded with ENC/FER1-RECEIPT/1.","descriptor_sha256":"d54df53834342b12b38efed5e178a34688b1cfa173e4a9a86a9b6052dd7fdc20"}

src/near_core/enc/fer1_receipt.c

@@ -0,0 +1,629 @@
+#include "amduat/enc/fer1_receipt.h"
+
+#include "amduat/enc/asl1_core_codec.h"
+#include "amduat/hash/asl1.h"
+
+#include <limits.h>
+#include <stdbool.h>
+#include <stdlib.h>
+#include <string.h>
+
+typedef struct {
+  const uint8_t *data;
+  size_t len;
+  size_t offset;
+} amduat_cursor_t;
+
+static void amduat_store_u16_be(uint8_t *out, uint16_t value) {
+  out[0] = (uint8_t)((value >> 8) & 0xffu);
+  out[1] = (uint8_t)(value & 0xffu);
+}
+
+static void amduat_store_u32_be(uint8_t *out, uint32_t value) {
+  out[0] = (uint8_t)((value >> 24) & 0xffu);
+  out[1] = (uint8_t)((value >> 16) & 0xffu);
+  out[2] = (uint8_t)((value >> 8) & 0xffu);
+  out[3] = (uint8_t)(value & 0xffu);
+}
+
+static void amduat_store_u64_be(uint8_t *out, uint64_t value) {
+  out[0] = (uint8_t)((value >> 56) & 0xffu);
+  out[1] = (uint8_t)((value >> 48) & 0xffu);
+  out[2] = (uint8_t)((value >> 40) & 0xffu);
+  out[3] = (uint8_t)((value >> 32) & 0xffu);
+  out[4] = (uint8_t)((value >> 24) & 0xffu);
+  out[5] = (uint8_t)((value >> 16) & 0xffu);
+  out[6] = (uint8_t)((value >> 8) & 0xffu);
+  out[7] = (uint8_t)(value & 0xffu);
+}
+
+static bool amduat_read_u8(amduat_cursor_t *cur, uint8_t *out) {
+  if (cur->len - cur->offset < 1) {
+    return false;
+  }
+  *out = cur->data[cur->offset];
+  cur->offset += 1;
+  return true;
+}
+
+static bool amduat_read_u16(amduat_cursor_t *cur, uint16_t *out) {
+  const uint8_t *data;
+  if (cur->len - cur->offset < 2) {
+    return false;
+  }
+  data = cur->data + cur->offset;
+  *out = (uint16_t)((data[0] << 8) | data[1]);
+  cur->offset += 2;
+  return true;
+}
+
+static bool amduat_read_u32(amduat_cursor_t *cur, uint32_t *out) {
+  const uint8_t *data;
+  if (cur->len - cur->offset < 4) {
+    return false;
+  }
+  data = cur->data + cur->offset;
+  *out = ((uint32_t)data[0] << 24) | ((uint32_t)data[1] << 16) |
+         ((uint32_t)data[2] << 8) | (uint32_t)data[3];
+  cur->offset += 4;
+  return true;
+}
+
+static bool amduat_read_u64(amduat_cursor_t *cur, uint64_t *out) {
+  const uint8_t *data;
+  if (cur->len - cur->offset < 8) {
+    return false;
+  }
+  data = cur->data + cur->offset;
+  *out = ((uint64_t)data[0] << 56) | ((uint64_t)data[1] << 48) |
+         ((uint64_t)data[2] << 40) | ((uint64_t)data[3] << 32) |
+         ((uint64_t)data[4] << 24) | ((uint64_t)data[5] << 16) |
+         ((uint64_t)data[6] << 8) | (uint64_t)data[7];
+  cur->offset += 8;
+  return true;
+}
+
+static bool amduat_add_size(size_t *acc, size_t add) {
+  if (*acc > SIZE_MAX - add) {
+    return false;
+  }
+  *acc += add;
+  return true;
+}
+
+static bool amduat_reference_bytes_len(amduat_reference_t ref, size_t *out_len) {
+  const amduat_hash_asl1_desc_t *desc;
+
+  if (ref.digest.len != 0 && ref.digest.data == NULL) {
+    return false;
+  }
+  if (amduat_hash_asl1_is_reserved(ref.hash_id)) {
+    return false;
+  }
+
+  desc = amduat_hash_asl1_desc_lookup(ref.hash_id);
+  if (desc != NULL && desc->digest_len != 0 &&
+      ref.digest.len != desc->digest_len) {
+    return false;
+  }
+
+  *out_len = 2 + ref.digest.len;
+  return true;
+}
+
+static int amduat_reference_cmp(amduat_reference_t a, amduat_reference_t b) {
+  size_t len_a = 2 + a.digest.len;
+  size_t len_b = 2 + b.digest.len;
+  size_t min_len;
+  int cmp;
+
+  if (len_a != len_b) {
+    return len_a < len_b ? -1 : 1;
+  }
+  if (a.hash_id != b.hash_id) {
+    return a.hash_id < b.hash_id ? -1 : 1;
+  }
+  min_len = a.digest.len < b.digest.len ? a.digest.len : b.digest.len;
+  if (min_len != 0) {
+    cmp = memcmp(a.digest.data, b.digest.data, min_len);
+    if (cmp != 0) {
+      return cmp;
+    }
+  }
+  if (a.digest.len != b.digest.len) {
+    return a.digest.len < b.digest.len ? -1 : 1;
+  }
+  return 0;
+}
+
+static bool amduat_encoded_ref_len(amduat_reference_t ref, size_t *out_len) {
+  size_t ref_len;
+
+  if (!amduat_reference_bytes_len(ref, &ref_len)) {
+    return false;
+  }
+  if (ref_len > UINT32_MAX) {
+    return false;
+  }
+  *out_len = 4 + ref_len;
+  return true;
+}
+
+static bool amduat_write_encoded_ref(uint8_t *buffer,
+                                     size_t buffer_len,
+                                     size_t *offset,
+                                     amduat_reference_t ref) {
+  size_t ref_len;
+
+  if (!amduat_reference_bytes_len(ref, &ref_len)) {
+    return false;
+  }
+  if (ref_len > UINT32_MAX) {
+    return false;
+  }
+  if (buffer_len - *offset < 4 + ref_len) {
+    return false;
+  }
+
+  amduat_store_u32_be(buffer + *offset, (uint32_t)ref_len);
+  *offset += 4;
+  amduat_store_u16_be(buffer + *offset, ref.hash_id);
+  *offset += 2;
+  if (ref.digest.len != 0) {
+    memcpy(buffer + *offset, ref.digest.data, ref.digest.len);
+    *offset += ref.digest.len;
+  }
+
+  return true;
+}
+
+static bool amduat_read_encoded_ref(amduat_cursor_t *cur,
+                                    amduat_reference_t *out_ref) {
+  uint32_t ref_len_u32;
+  amduat_octets_t ref_bytes;
+
+  if (!amduat_read_u32(cur, &ref_len_u32)) {
+    return false;
+  }
+  if (ref_len_u32 < 2) {
+    return false;
+  }
+  if (cur->len - cur->offset < ref_len_u32) {
+    return false;
+  }
+  ref_bytes = amduat_octets(cur->data + cur->offset, ref_len_u32);
+  if (!amduat_enc_asl1_core_decode_reference_v1(ref_bytes, out_ref)) {
+    return false;
+  }
+  cur->offset += ref_len_u32;
+  return true;
+}
+
+void amduat_enc_fer1_receipt_free(amduat_fer1_receipt_t *receipt) {
+  size_t i;
+
+  if (receipt == NULL) {
+    return;
+  }
+
+  amduat_reference_free(&receipt->function_ref);
+  amduat_reference_free(&receipt->input_manifest_ref);
+  amduat_reference_free(&receipt->environment_ref);
+  amduat_reference_free(&receipt->output_ref);
+  amduat_octets_free(&receipt->evaluator_id);
+
+  if (receipt->executor_refs != NULL) {
+    for (i = 0; i < receipt->executor_refs_len; ++i) {
+      amduat_reference_free(&receipt->executor_refs[i]);
+    }
+    free(receipt->executor_refs);
+  }
+
+  if (receipt->parity != NULL) {
+    for (i = 0; i < receipt->parity_len; ++i) {
+      amduat_reference_free(&receipt->parity[i].executor_ref);
+      amduat_reference_free(&receipt->parity[i].output_ref);
+      if (receipt->parity[i].has_sbom_ref) {
+        amduat_reference_free(&receipt->parity[i].sbom_ref);
+      }
+      amduat_octets_free(&receipt->parity[i].parity_digest);
+    }
+    free(receipt->parity);
+  }
+
+  receipt->executor_refs = NULL;
+  receipt->executor_refs_len = 0;
+  receipt->parity = NULL;
+  receipt->parity_len = 0;
+}
+
+bool amduat_enc_fer1_receipt_encode_v1(
+    const amduat_fer1_receipt_t *receipt,
+    amduat_octets_t *out_bytes) {
+  size_t total_len = 0;
+  size_t offset = 0;
+  uint8_t *buffer;
+  size_t i;
+
+  if (receipt == NULL || out_bytes == NULL) {
+    return false;
+  }
+  out_bytes->data = NULL;
+  out_bytes->len = 0;
+
+  if (receipt->fer1_version != 1) {
+    return false;
+  }
+  if (receipt->evaluator_id.len != 0 && receipt->evaluator_id.data == NULL) {
+    return false;
+  }
+  if (receipt->executor_refs_len != 0 && receipt->executor_refs == NULL) {
+    return false;
+  }
+  if (receipt->parity_len != 0 && receipt->parity == NULL) {
+    return false;
+  }
+  if (receipt->executor_refs_len != receipt->parity_len) {
+    return false;
+  }
+  if (receipt->evaluator_id.len > UINT32_MAX) {
+    return false;
+  }
+  if (receipt->started_at > receipt->completed_at) {
+    return false;
+  }
+  for (i = 1; i < receipt->executor_refs_len; ++i) {
+    if (amduat_reference_cmp(receipt->executor_refs[i - 1],
+                             receipt->executor_refs[i]) > 0) {
+      return false;
+    }
+  }
+  for (i = 0; i < receipt->parity_len; ++i) {
+    if (!amduat_reference_eq(receipt->parity[i].executor_ref,
+                             receipt->executor_refs[i])) {
+      return false;
+    }
+    if (i > 0 &&
+        amduat_reference_cmp(receipt->parity[i - 1].executor_ref,
+                             receipt->parity[i].executor_ref) > 0) {
+      return false;
+    }
+  }
+
+  {
+    size_t enc_len;
+    if (!amduat_add_size(&total_len, 2) ||
+        !amduat_encoded_ref_len(receipt->function_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len) ||
+        !amduat_encoded_ref_len(receipt->input_manifest_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len) ||
+        !amduat_encoded_ref_len(receipt->environment_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len)) {
+      return false;
+    }
+  }
+
+  if (!amduat_add_size(&total_len, 4 + receipt->evaluator_id.len)) {
+    return false;
+  }
+
+  {
+    size_t enc_len;
+    if (!amduat_encoded_ref_len(receipt->output_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len)) {
+      return false;
+    }
+  }
+
+  if (!amduat_add_size(&total_len, 4)) {
+    return false;
+  }
+  for (i = 0; i < receipt->executor_refs_len; ++i) {
+    size_t enc_len;
+    if (!amduat_encoded_ref_len(receipt->executor_refs[i], &enc_len) ||
+        !amduat_add_size(&total_len, enc_len)) {
+      return false;
+    }
+  }
+
+  if (!amduat_add_size(&total_len, 4)) {
+    return false;
+  }
+  for (i = 0; i < receipt->parity_len; ++i) {
+    size_t enc_len;
+    const amduat_fer1_parity_entry_t *entry = &receipt->parity[i];
+    if (entry->parity_digest.len != 0 &&
+        entry->parity_digest.data == NULL) {
+      return false;
+    }
+    if (entry->parity_digest.len > UINT32_MAX) {
+      return false;
+    }
+    if (!amduat_reference_eq(entry->output_ref, receipt->output_ref)) {
+      return false;
+    }
+    if (!amduat_encoded_ref_len(entry->executor_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len) ||
+        !amduat_encoded_ref_len(entry->output_ref, &enc_len) ||
+        !amduat_add_size(&total_len, enc_len) ||
+        !amduat_add_size(&total_len, 1)) {
+      return false;
+    }
+    if (entry->has_sbom_ref) {
+      if (!amduat_encoded_ref_len(entry->sbom_ref, &enc_len) ||
+          !amduat_add_size(&total_len, enc_len)) {
+        return false;
+      }
+    }
+    if (!amduat_add_size(&total_len, 4 + entry->parity_digest.len)) {
+      return false;
+    }
+  }
+
+  if (!amduat_add_size(&total_len, 8 + 8)) {
+    return false;
+  }
+
+  buffer = (uint8_t *)malloc(total_len);
+  if (buffer == NULL) {
+    return false;
+  }
+
+  amduat_store_u16_be(buffer + offset, receipt->fer1_version);
+  offset += 2;
+
+  if (!amduat_write_encoded_ref(buffer, total_len, &offset,
+                                receipt->function_ref) ||
+      !amduat_write_encoded_ref(buffer, total_len, &offset,
+                                receipt->input_manifest_ref) ||
+      !amduat_write_encoded_ref(buffer, total_len, &offset,
+                                receipt->environment_ref)) {
+    free(buffer);
+    return false;
+  }
+
+  amduat_store_u32_be(buffer + offset, (uint32_t)receipt->evaluator_id.len);
+  offset += 4;
+  if (receipt->evaluator_id.len != 0) {
+    memcpy(buffer + offset, receipt->evaluator_id.data,
+           receipt->evaluator_id.len);
+    offset += receipt->evaluator_id.len;
+  }
+
+  if (!amduat_write_encoded_ref(buffer, total_len, &offset,
+                                receipt->output_ref)) {
+    free(buffer);
+    return false;
+  }
+
+  amduat_store_u32_be(buffer + offset, (uint32_t)receipt->executor_refs_len);
+  offset += 4;
+  for (i = 0; i < receipt->executor_refs_len; ++i) {
+    if (!amduat_write_encoded_ref(buffer, total_len, &offset,
+                                  receipt->executor_refs[i])) {
+      free(buffer);
+      return false;
+    }
+  }
+
+  amduat_store_u32_be(buffer + offset, (uint32_t)receipt->parity_len);
+  offset += 4;
+  for (i = 0; i < receipt->parity_len; ++i) {
+    const amduat_fer1_parity_entry_t *entry = &receipt->parity[i];
+    if (!amduat_write_encoded_ref(buffer, total_len, &offset,
+                                  entry->executor_ref) ||
+        !amduat_write_encoded_ref(buffer, total_len, &offset,
+                                  entry->output_ref)) {
+      free(buffer);
+      return false;
+    }
+    buffer[offset++] = entry->has_sbom_ref ? 0x01u : 0x00u;
+    if (entry->has_sbom_ref) {
+      if (!amduat_write_encoded_ref(buffer, total_len, &offset,
+                                    entry->sbom_ref)) {
+        free(buffer);
+        return false;
+      }
+    }
+    amduat_store_u32_be(buffer + offset, (uint32_t)entry->parity_digest.len);
+    offset += 4;
+    if (entry->parity_digest.len != 0) {
+      memcpy(buffer + offset, entry->parity_digest.data,
+             entry->parity_digest.len);
+      offset += entry->parity_digest.len;
+    }
+  }
+
+  amduat_store_u64_be(buffer + offset, receipt->started_at);
+  offset += 8;
+  amduat_store_u64_be(buffer + offset, receipt->completed_at);
+  offset += 8;
+
+  out_bytes->data = buffer;
+  out_bytes->len = total_len;
+  return true;
+}
+
+bool amduat_enc_fer1_receipt_decode_v1(
+    amduat_octets_t bytes,
+    amduat_fer1_receipt_t *out_receipt) {
+  amduat_cursor_t cur;
+  uint16_t fer1_version;
+  uint32_t len_u32;
+  uint32_t executor_count;
+  uint32_t parity_count;
+  size_t i;
+
+  if (out_receipt == NULL) {
+    return false;
+  }
+  if (bytes.len != 0 && bytes.data == NULL) {
+    return false;
+  }
+
+  memset(out_receipt, 0, sizeof(*out_receipt));
+
+  cur.data = bytes.data;
+  cur.len = bytes.len;
+  cur.offset = 0;
+
+  if (!amduat_read_u16(&cur, &fer1_version)) {
+    return false;
+  }
+  if (fer1_version != 1) {
+    return false;
+  }
+  out_receipt->fer1_version = fer1_version;
+
+  if (!amduat_read_encoded_ref(&cur, &out_receipt->function_ref) ||
+      !amduat_read_encoded_ref(&cur, &out_receipt->input_manifest_ref) ||
+      !amduat_read_encoded_ref(&cur, &out_receipt->environment_ref)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+
+  if (!amduat_read_u32(&cur, &len_u32)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (cur.len - cur.offset < len_u32) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (len_u32 != 0) {
+    amduat_octets_t src = amduat_octets(cur.data + cur.offset, len_u32);
+    if (!amduat_octets_clone(src, &out_receipt->evaluator_id)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    cur.offset += len_u32;
+  }
+
+  if (!amduat_read_encoded_ref(&cur, &out_receipt->output_ref)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+
+  if (!amduat_read_u32(&cur, &executor_count)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (executor_count != 0) {
+    if (executor_count > SIZE_MAX / sizeof(amduat_reference_t)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    out_receipt->executor_refs =
+        (amduat_reference_t *)calloc(executor_count,
+                                     sizeof(amduat_reference_t));
+    if (out_receipt->executor_refs == NULL) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+  }
+  out_receipt->executor_refs_len = executor_count;
+
+  for (i = 0; i < out_receipt->executor_refs_len; ++i) {
+    if (!amduat_read_encoded_ref(&cur, &out_receipt->executor_refs[i])) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+  }
+  for (i = 1; i < out_receipt->executor_refs_len; ++i) {
+    if (amduat_reference_cmp(out_receipt->executor_refs[i - 1],
+                             out_receipt->executor_refs[i]) > 0) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+  }
+
+  if (!amduat_read_u32(&cur, &parity_count)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (parity_count != executor_count) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (parity_count != 0) {
+    if (parity_count > SIZE_MAX / sizeof(amduat_fer1_parity_entry_t)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    out_receipt->parity =
+        (amduat_fer1_parity_entry_t *)calloc(
+            parity_count, sizeof(amduat_fer1_parity_entry_t));
+    if (out_receipt->parity == NULL) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+  }
+  out_receipt->parity_len = parity_count;
+
+  for (i = 0; i < out_receipt->parity_len; ++i) {
+    amduat_fer1_parity_entry_t *entry = &out_receipt->parity[i];
+    uint8_t has_sbom = 0;
+    uint32_t digest_len = 0;
+
+    if (!amduat_read_encoded_ref(&cur, &entry->executor_ref) ||
+        !amduat_read_encoded_ref(&cur, &entry->output_ref) ||
+        !amduat_read_u8(&cur, &has_sbom)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    if (!amduat_reference_eq(entry->executor_ref,
+                             out_receipt->executor_refs[i])) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    if (i > 0 &&
+        amduat_reference_cmp(out_receipt->parity[i - 1].executor_ref,
+                             entry->executor_ref) > 0) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    if (!amduat_reference_eq(entry->output_ref, out_receipt->output_ref)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    entry->has_sbom_ref = (has_sbom != 0);
+    if (entry->has_sbom_ref) {
+      if (!amduat_read_encoded_ref(&cur, &entry->sbom_ref)) {
+        amduat_enc_fer1_receipt_free(out_receipt);
+        return false;
+      }
+    }
+    if (!amduat_read_u32(&cur, &digest_len)) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    if (cur.len - cur.offset < digest_len) {
+      amduat_enc_fer1_receipt_free(out_receipt);
+      return false;
+    }
+    if (digest_len != 0) {
+      amduat_octets_t src = amduat_octets(cur.data + cur.offset, digest_len);
+      if (!amduat_octets_clone(src, &entry->parity_digest)) {
+        amduat_enc_fer1_receipt_free(out_receipt);
+        return false;
+      }
+      cur.offset += digest_len;
+    }
+  }
+
+  if (!amduat_read_u64(&cur, &out_receipt->started_at) ||
+      !amduat_read_u64(&cur, &out_receipt->completed_at)) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (out_receipt->started_at > out_receipt->completed_at) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+  if (cur.offset != cur.len) {
+    amduat_enc_fer1_receipt_free(out_receipt);
+    return false;
+  }
+
+  return true;
+}

src/near_core/fer/receipt.c

@@ -0,0 +1,75 @@
+#include "amduat/fer/receipt.h"
+
+#include "amduat/enc/fer1_receipt.h"
+
+#include <string.h>
+
+bool amduat_fer1_receipt_from_pel_result(
+    const amduat_pel_surface_execution_result_t *pel_result,
+    amduat_reference_t input_manifest_ref,
+    amduat_reference_t environment_ref,
+    amduat_octets_t evaluator_id,
+    amduat_reference_t executor_ref,
+    bool has_sbom_ref,
+    amduat_reference_t sbom_ref,
+    amduat_octets_t parity_digest,
+    uint64_t started_at,
+    uint64_t completed_at,
+    amduat_artifact_t *out_artifact) {
+  amduat_fer1_receipt_t receipt;
+  amduat_fer1_parity_entry_t parity;
+  amduat_reference_t executor_refs[1];
+  amduat_octets_t receipt_bytes;
+
+  if (out_artifact == NULL) {
+    return false;
+  }
+  *out_artifact = amduat_artifact(amduat_octets(NULL, 0u));
+
+  if (pel_result == NULL) {
+    return false;
+  }
+  if (pel_result->output_refs_len != 1 || pel_result->output_refs == NULL) {
+    return false;
+  }
+  if (evaluator_id.len != 0 && evaluator_id.data == NULL) {
+    return false;
+  }
+  if (parity_digest.len != 0 && parity_digest.data == NULL) {
+    return false;
+  }
+
+  memset(&receipt, 0, sizeof(receipt));
+  receipt.fer1_version = 1;
+  receipt.function_ref = pel_result->program_ref;
+  receipt.input_manifest_ref = input_manifest_ref;
+  receipt.environment_ref = environment_ref;
+  receipt.evaluator_id = evaluator_id;
+  receipt.output_ref = pel_result->output_refs[0];
+  receipt.started_at = started_at;
+  receipt.completed_at = completed_at;
+
+  executor_refs[0] = executor_ref;
+  receipt.executor_refs = executor_refs;
+  receipt.executor_refs_len = 1;
+
+  memset(&parity, 0, sizeof(parity));
+  parity.executor_ref = executor_ref;
+  parity.output_ref = receipt.output_ref;
+  parity.has_sbom_ref = has_sbom_ref;
+  if (has_sbom_ref) {
+    parity.sbom_ref = sbom_ref;
+  }
+  parity.parity_digest = parity_digest;
+  receipt.parity = &parity;
+  receipt.parity_len = 1;
+
+  if (!amduat_enc_fer1_receipt_encode_v1(&receipt, &receipt_bytes)) {
+    return false;
+  }
+
+  *out_artifact = amduat_artifact_with_type(
+      amduat_octets(receipt_bytes.data, receipt_bytes.len),
+      amduat_type_tag(AMDUAT_TYPE_TAG_FER1_RECEIPT_1));
+  return true;
+}

src/pel_stack/opreg/kernel_params.c

@@ -131,6 +131,8 @@ bool amduat_pel_kernel_params_decode(
       return amduat_decode_hash(params_bytes, &out_params->value.hash);
     case AMDUAT_PEL_KERNEL_OP_PARAMS:
       return amduat_decode_unit(params_bytes);
+    case AMDUAT_PEL_KERNEL_OP_FORMAT_ENCODE:
+      return amduat_decode_unit(params_bytes);
     default:
       return false;
   }

src/tools/amduat_pel_cli.c

@@ -141,7 +141,7 @@ static void amduat_pel_cli_print_usage(FILE *stream) {
           "  - Only PEL/PROGRAM-DAG/1 is supported; other scheme refs yield SCHEME_UNSUPPORTED.\n"
           "  - Expected type tags: program 0x00000101, trace 0x00000102, result 0x00000103.\n"
           "  - Encoding profile IDs: program 0x0101, trace 0x0102, result 0x0103.\n"
-          "  - Kernel ops: pel.bytes.concat, pel.bytes.slice, pel.bytes.const, pel.bytes.hash.asl1.\n"
+          "  - Kernel ops: pel.bytes.concat, pel.bytes.slice, pel.bytes.const, pel.bytes.hash.asl1, pel.format.encode.\n"
           "  - --ref-format bytes expects REF arguments to be a path or '-' (raw reference bytes).\n"
           "  - --inputs-file with --ref-format bytes expects raw concatenated references.\n");
 }

tests/enc/test_fer1_receipt.c

@@ -0,0 +1,275 @@
+#include "amduat/enc/fer1_receipt.h"
+#include "amduat/fer/receipt.h"
+
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+static const uint8_t k_expected_receipt_bytes[] = {
+    0x00, 0x01, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x00, 0x00, 0x00, 0x06,
+    0x74, 0x65, 0x73, 0x74, 0x65, 0x72, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x00, 0x00, 0x00, 0x02,
+    0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x51, 0x51, 0x51, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x22,
+    0x00, 0x01, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x00, 0x00,
+    0x00, 0x22, 0x00, 0x01, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x01, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x60, 0x60, 0x60, 0x60, 0x60,
+    0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60,
+    0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60, 0x60,
+    0x60, 0x60, 0x60, 0x60, 0x00, 0x00, 0x00, 0x03, 0xaa, 0xbb, 0xcc, 0x00,
+    0x00, 0x00, 0x22, 0x00, 0x01, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51, 0x51,
+    0x51, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+    0x00, 0x00, 0x00, 0x00, 0x00, 0x0a, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+    0x00, 0x14,
+};
+
+static const uint8_t k_expected_receipt_helper_bytes[] = {
+    0x00, 0x01, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11, 0x11,
+    0x11, 0x11, 0x11, 0x11, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22,
+    0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33,
+    0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x33, 0x00, 0x00, 0x00, 0x06,
+    0x74, 0x65, 0x73, 0x74, 0x65, 0x72, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x00, 0x00, 0x00, 0x01,
+    0x00, 0x00, 0x00, 0x22, 0x00, 0x01, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x22, 0x00, 0x01,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50,
+    0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x50, 0x00, 0x00, 0x00, 0x22,
+    0x00, 0x01, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44,
+    0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x44, 0x00, 0x00,
+    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0a, 0x00,
+    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x14,
+};
+
+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 bool bytes_equal(amduat_octets_t bytes,
+                        const uint8_t *expected,
+                        size_t expected_len) {
+  if (bytes.len != expected_len) {
+    return false;
+  }
+  if (bytes.len == 0) {
+    return true;
+  }
+  return memcmp(bytes.data, expected, expected_len) == 0;
+}
+
+static int test_receipt_round_trip(void) {
+  amduat_fer1_receipt_t receipt;
+  amduat_octets_t encoded;
+  amduat_fer1_receipt_t decoded;
+  amduat_reference_t executor_refs[2];
+  amduat_fer1_parity_entry_t parity[2];
+  uint8_t f0[32], i0[32], e0[32], o0[32];
+  uint8_t ex0[32], ex1[32], sb0[32];
+  uint8_t digest0[] = {0xaa, 0xbb, 0xcc};
+  int exit_code = 1;
+
+  memset(&receipt, 0, sizeof(receipt));
+  receipt.fer1_version = 1;
+  receipt.function_ref = make_ref(0x11, f0);
+  receipt.input_manifest_ref = make_ref(0x22, i0);
+  receipt.environment_ref = make_ref(0x33, e0);
+  receipt.evaluator_id = amduat_octets("tester", 6);
+  receipt.output_ref = make_ref(0x44, o0);
+  receipt.started_at = 10;
+  receipt.completed_at = 20;
+
+  executor_refs[0] = make_ref(0x50, ex0);
+  executor_refs[1] = make_ref(0x51, ex1);
+  receipt.executor_refs = executor_refs;
+  receipt.executor_refs_len = 2;
+
+  memset(parity, 0, sizeof(parity));
+  parity[0].executor_ref = executor_refs[0];
+  parity[0].output_ref = receipt.output_ref;
+  parity[0].has_sbom_ref = true;
+  parity[0].sbom_ref = make_ref(0x60, sb0);
+  parity[0].parity_digest = amduat_octets(digest0, sizeof(digest0));
+
+  parity[1].executor_ref = executor_refs[1];
+  parity[1].output_ref = receipt.output_ref;
+  parity[1].has_sbom_ref = false;
+  parity[1].parity_digest = amduat_octets(NULL, 0);
+
+  receipt.parity = parity;
+  receipt.parity_len = 2;
+
+  if (!amduat_enc_fer1_receipt_encode_v1(&receipt, &encoded)) {
+    fprintf(stderr, "encode failed\n");
+    return exit_code;
+  }
+
+  if (!bytes_equal(encoded, k_expected_receipt_bytes,
+                   sizeof(k_expected_receipt_bytes))) {
+    fprintf(stderr, "encoded bytes mismatch\n");
+    goto cleanup;
+  }
+
+  if (!amduat_enc_fer1_receipt_decode_v1(encoded, &decoded)) {
+    fprintf(stderr, "decode failed\n");
+    goto cleanup;
+  }
+
+  if (!amduat_reference_eq(decoded.function_ref, receipt.function_ref) ||
+      !amduat_reference_eq(decoded.input_manifest_ref,
+                           receipt.input_manifest_ref) ||
+      !amduat_reference_eq(decoded.environment_ref,
+                           receipt.environment_ref) ||
+      !amduat_reference_eq(decoded.output_ref, receipt.output_ref)) {
+    fprintf(stderr, "decoded refs mismatch\n");
+    goto cleanup_decoded;
+  }
+
+  if (!amduat_octets_eq(decoded.evaluator_id, receipt.evaluator_id) ||
+      decoded.executor_refs_len != 2 || decoded.parity_len != 2 ||
+      decoded.started_at != receipt.started_at ||
+      decoded.completed_at != receipt.completed_at) {
+    fprintf(stderr, "decoded fields mismatch\n");
+    goto cleanup_decoded;
+  }
+
+  if (!amduat_reference_eq(decoded.executor_refs[0], executor_refs[0]) ||
+      !amduat_reference_eq(decoded.executor_refs[1], executor_refs[1]) ||
+      !amduat_reference_eq(decoded.parity[0].executor_ref, executor_refs[0]) ||
+      !amduat_reference_eq(decoded.parity[0].output_ref,
+                           receipt.output_ref) ||
+      !decoded.parity[0].has_sbom_ref ||
+      !amduat_reference_eq(decoded.parity[0].sbom_ref, parity[0].sbom_ref) ||
+      !amduat_octets_eq(decoded.parity[0].parity_digest,
+                        parity[0].parity_digest) ||
+      !amduat_reference_eq(decoded.parity[1].executor_ref, executor_refs[1]) ||
+      !amduat_reference_eq(decoded.parity[1].output_ref,
+                           receipt.output_ref) ||
+      decoded.parity[1].has_sbom_ref ||
+      decoded.parity[1].parity_digest.len != 0) {
+    fprintf(stderr, "decoded parity mismatch\n");
+    goto cleanup_decoded;
+  }
+
+  exit_code = 0;
+
+cleanup_decoded:
+  amduat_enc_fer1_receipt_free(&decoded);
+cleanup:
+  free((void *)encoded.data);
+  return exit_code;
+}
+
+static int test_invalid_receipt_version(void) {
+  uint8_t bad_bytes[sizeof(k_expected_receipt_bytes)];
+  amduat_octets_t bytes;
+  amduat_fer1_receipt_t decoded;
+
+  memcpy(bad_bytes, k_expected_receipt_bytes, sizeof(bad_bytes));
+  bad_bytes[1] = 0x02;
+
+  bytes = amduat_octets(bad_bytes, sizeof(bad_bytes));
+  if (amduat_enc_fer1_receipt_decode_v1(bytes, &decoded)) {
+    fprintf(stderr, "invalid receipt version accepted\n");
+    amduat_enc_fer1_receipt_free(&decoded);
+    return 1;
+  }
+
+  return 0;
+}
+
+static int test_receipt_helper(void) {
+  amduat_pel_surface_execution_result_t pel_result;
+  amduat_artifact_t artifact;
+  amduat_reference_t output_ref;
+  uint8_t f0[32], i0[32], e0[32], o0[32];
+  uint8_t ex0[32];
+
+  memset(&pel_result, 0, sizeof(pel_result));
+  pel_result.pel1_version = 1;
+  pel_result.program_ref = make_ref(0x11, f0);
+  pel_result.output_refs = &output_ref;
+  pel_result.output_refs_len = 1;
+  output_ref = make_ref(0x44, o0);
+
+  if (!amduat_fer1_receipt_from_pel_result(
+          &pel_result,
+          make_ref(0x22, i0),
+          make_ref(0x33, e0),
+          amduat_octets("tester", 6),
+          make_ref(0x50, ex0),
+          false,
+          amduat_reference(0, amduat_octets(NULL, 0)),
+          amduat_octets(NULL, 0),
+          10,
+          20,
+          &artifact)) {
+    fprintf(stderr, "helper failed\n");
+    return 1;
+  }
+
+  if (!bytes_equal(artifact.bytes, k_expected_receipt_helper_bytes,
+                   sizeof(k_expected_receipt_helper_bytes))) {
+    fprintf(stderr, "helper bytes mismatch\n");
+    amduat_artifact_free(&artifact);
+    return 1;
+  }
+
+  amduat_artifact_free(&artifact);
+  return 0;
+}
+
+int main(void) {
+  if (test_receipt_round_trip() != 0) {
+    return 1;
+  }
+  if (test_invalid_receipt_version() != 0) {
+    return 1;
+  }
+  if (test_receipt_helper() != 0) {
+    return 1;
+  }
+  return 0;
+}

tier1/enc-fer1-receipt-1.md

@@ -0,0 +1,111 @@
+# ENC/FER1-RECEIPT/1 — Canonical Encoding for FER/1 Receipts
+
+Status: Draft
+Owner: Architecture
+Version: 0.1.0
+SoT: Yes
+Last Updated: 2025-12-01
+Linked Phase Pack: PH07
+Tags: [evidence, receipt, deterministic, execution]
+
+**Document ID:** `ENC/FER1-RECEIPT/1`
+**Profile ID:** `FER_ENC_RECEIPT_V1 = 0x0301`
+**TypeTag:** `TYPE_TAG_FER1_RECEIPT_1 = 0x00000301`
+
+**Depends on (normative):**
+
+* `ASL/1-CORE v0.4.x` — value model (`Artifact`, `Reference`, `OctetString`)
+* `ENC/ASL1-CORE v1.0.x` — canonical encoding for `Reference`
+* `FER/1` — receipt semantics and required fields
+
+---
+
+## 0. Overview
+
+`ENC/FER1-RECEIPT/1` defines the canonical binary encoding for FER/1 receipts.
+Receipts are stored as ASL/1 Artifacts with:
+
+```
+Artifact.type_tag = TYPE_TAG_FER1_RECEIPT_1
+Artifact.bytes    = ReceiptBytes
+```
+
+This encoding is deterministic and injective. Ordering is fixed and list
+ordering is required for canonicalization.
+
+---
+
+## 1. ReceiptBytes Layout (v1)
+
+All integers are **big-endian**. Lengths are unsigned.
+
+```
+ReceiptBytes =
+  fer1_version         : U16
+  function_ref         : EncodedRef
+  input_manifest_ref   : EncodedRef
+  environment_ref      : EncodedRef
+  evaluator_id_len     : U32
+  evaluator_id_bytes   : BYTES
+  output_ref           : EncodedRef
+  executor_count       : U32
+  executor_refs        : EncodedRef[executor_count]
+  parity_count         : U32
+  parity_entries       : ParityEntry[parity_count]
+  started_at           : U64
+  completed_at         : U64
+```
+
+Rules (normative):
+
+* `fer1_version` MUST be `0x0001`.
+* `parity_count` MUST equal `executor_count`.
+* Every `ParityEntry.output_ref` MUST equal the top-level `output_ref`.
+* `parity_entries[i].executor_ref` MUST equal `executor_refs[i]`.
+* `started_at` MUST be less than or equal to `completed_at`.
+* `executor_refs` and `parity_entries` MUST be ordered by ascending
+  `EncodedRef` byte order to ensure canonicalization.
+
+---
+
+## 2. EncodedRef
+
+`EncodedRef` embeds an ASL/1 `Reference` using a length prefix:
+
+```
+EncodedRef =
+  ref_len   : U32
+  ref_bytes : BYTES   // ReferenceBytes (ENC/ASL1-CORE v1)
+```
+
+`ref_len` is the length of `ReferenceBytes`. `ReferenceBytes` uses the
+canonical encoding from `ENC/ASL1-CORE v1`.
+
+---
+
+## 3. ParityEntry
+
+```
+ParityEntry =
+  executor_ref      : EncodedRef
+  output_ref        : EncodedRef
+  has_sbom_ref      : U8
+  sbom_ref?         : EncodedRef  // if has_sbom_ref == 1
+  parity_digest_len : U32
+  parity_digest     : BYTES
+```
+
+`parity_digest` is an opaque, executor-specific digest. Empty digests are
+allowed (`parity_digest_len = 0`).
+
+---
+
+## 4. Canonicalization and Validation
+
+Implementations MUST:
+
+* enforce list ordering for `executor_refs` and `parity_entries`,
+* reject truncated payloads or trailing bytes, and
+* reject any receipt where required references are malformed or invalid.
+
+No other metadata or policy is embedded in the receipt bytes.