Definition serializeValue (v : componentValueT) : list octet :=
  match v with
  | ValueIntegerS8 v      => octets8 (s8 v)
  | ValueIntegerS8Vec2 v  => octets8 (s8vec2_0 v) ++ octets8 (s8vec2_1 v)
  | ValueIntegerS8Vec3 v  => octets8 (s8vec3_0 v) ++ octets8 (s8vec3_1 v) ++ octets8 (s8vec3_2 v)
  | ValueIntegerS8Vec4 v  => octets8 (s8vec4_0 v) ++ octets8 (s8vec4_1 v) ++ octets8 (s8vec4_2 v) ++ octets8 (s8vec4_3 v)
  | ValueIntegerU8 v      => octets8 (u8 v)
  | ValueIntegerU8Vec2 v  => octets8 (u8vec2_0 v) ++ octets8 (u8vec2_1 v)
  | ValueIntegerU8Vec3 v  => octets8 (u8vec3_0 v) ++ octets8 (u8vec3_1 v) ++ octets8 (u8vec3_2 v)
  | ValueIntegerU8Vec4 v  => octets8 (u8vec4_0 v) ++ octets8 (u8vec4_1 v) ++ octets8 (u8vec4_2 v) ++ octets8 (u8vec4_3 v)
  | ValueIntegerS16 v     => octets16BE (s16 v)
  | ValueIntegerS16Vec2 v => octets16BE (s16vec2_0 v) ++ octets16BE (s16vec2_1 v)
  | ValueIntegerS16Vec3 v => octets16BE (s16vec3_0 v) ++ octets16BE (s16vec3_1 v) ++ octets16BE (s16vec3_2 v)
  | ValueIntegerS16Vec4 v => octets16BE (s16vec4_0 v) ++ octets16BE (s16vec4_1 v) ++ octets16BE (s16vec4_2 v) ++ octets16BE (s16vec4_3 v)
  | ValueIntegerU16 v     => octets16BE (u16 v)
  | ValueIntegerU16Vec2 v => octets16BE (u16vec2_0 v) ++ octets16BE (u16vec2_1 v)
  | ValueIntegerU16Vec3 v => octets16BE (u16vec3_0 v) ++ octets16BE (u16vec3_1 v) ++ octets16BE (u16vec3_2 v)
  | ValueIntegerU16Vec4 v => octets16BE (u16vec4_0 v) ++ octets16BE (u16vec4_1 v) ++ octets16BE (u16vec4_2 v) ++ octets16BE (u16vec4_3 v)
  | ValueIntegerS32 v     => octets32BE (s32 v)
  | ValueIntegerS32Vec2 v => octets32BE (s32vec2_0 v) ++ octets32BE (s32vec2_1 v)
  | ValueIntegerS32Vec3 v => octets32BE (s32vec3_0 v) ++ octets32BE (s32vec3_1 v) ++ octets32BE (s32vec3_2 v)
  | ValueIntegerS32Vec4 v => octets32BE (s32vec4_0 v) ++ octets32BE (s32vec4_1 v) ++ octets32BE (s32vec4_2 v) ++ octets32BE (s32vec4_3 v)
  | ValueIntegerU32 v     => octets32BE (u32 v)
  | ValueIntegerU32Vec2 v => octets32BE (u32vec2_0 v) ++ octets32BE (u32vec2_1 v)
  | ValueIntegerU32Vec3 v => octets32BE (u32vec3_0 v) ++ octets32BE (u32vec3_1 v) ++ octets32BE (u32vec3_2 v)
  | ValueIntegerU32Vec4 v => octets32BE (u32vec4_0 v) ++ octets32BE (u32vec4_1 v) ++ octets32BE (u32vec4_2 v) ++ octets32BE (u32vec4_3 v)
  | ValueIntegerS64 v     => octets64BE (s64 v)
  | ValueIntegerS64Vec2 v => octets64BE (s64vec2_0 v) ++ octets64BE (s64vec2_1 v)
  | ValueIntegerS64Vec3 v => octets64BE (s64vec3_0 v) ++ octets64BE (s64vec3_1 v) ++ octets64BE (s64vec3_2 v)
  | ValueIntegerS64Vec4 v => octets64BE (s64vec4_0 v) ++ octets64BE (s64vec4_1 v) ++ octets64BE (s64vec4_2 v) ++ octets64BE (s64vec4_3 v)
  | ValueIntegerU64 v     => octets64BE (u64 v)
  | ValueIntegerU64Vec2 v => octets64BE (u64vec2_0 v) ++ octets64BE (u64vec2_1 v)
  | ValueIntegerU64Vec3 v => octets64BE (u64vec3_0 v) ++ octets64BE (u64vec3_1 v) ++ octets64BE (u64vec3_2 v)
  | ValueIntegerU64Vec4 v => octets64BE (u64vec4_0 v) ++ octets64BE (u64vec4_1 v) ++ octets64BE (u64vec4_2 v) ++ octets64BE (u64vec4_3 v)
  | ValueFloat16 v        => octets16BE (float16BitsOf (f16 v))
  | ValueFloat16Vec2 v    => octets16BE (float16BitsOf (f16vec2_0 v)) ++ octets16BE (float16BitsOf (f16vec2_1 v))
  | ValueFloat16Vec3 v    => octets16BE (float16BitsOf (f16vec3_0 v)) ++ octets16BE (float16BitsOf (f16vec3_1 v)) ++ octets16BE (float16BitsOf (f16vec3_2 v))
  | ValueFloat16Vec4 v    => octets16BE (float16BitsOf (f16vec4_0 v)) ++ octets16BE (float16BitsOf (f16vec4_1 v)) ++ octets16BE (float16BitsOf (f16vec4_2 v)) ++ octets16BE (float16BitsOf (f16vec4_3 v))
  | ValueFloat32 v        => octets32BE (float32BitsOf (f32 v))
  | ValueFloat32Vec2 v    => octets32BE (float32BitsOf (f32vec2_0 v)) ++ octets32BE (float32BitsOf (f32vec2_1 v))
  | ValueFloat32Vec3 v    => octets32BE (float32BitsOf (f32vec3_0 v)) ++ octets32BE (float32BitsOf (f32vec3_1 v)) ++ octets32BE (float32BitsOf (f32vec3_2 v))
  | ValueFloat32Vec4 v    => octets32BE (float32BitsOf (f32vec4_0 v)) ++ octets32BE (float32BitsOf (f32vec4_1 v)) ++ octets32BE (float32BitsOf (f32vec4_2 v)) ++ octets32BE (float32BitsOf (f32vec4_3 v))
  | ValueFloat64 v        => octets64BE (float64BitsOf (f64 v))
  | ValueFloat64Vec2 v    => octets64BE (float64BitsOf (f64vec2_0 v)) ++ octets64BE (float64BitsOf (f64vec2_1 v))
  | ValueFloat64Vec3 v    => octets64BE (float64BitsOf (f64vec3_0 v)) ++ octets64BE (float64BitsOf (f64vec3_1 v)) ++ octets64BE (float64BitsOf (f64vec3_2 v))
  | ValueFloat64Vec4 v    => octets64BE (float64BitsOf (f64vec4_0 v)) ++ octets64BE (float64BitsOf (f64vec4_1 v)) ++ octets64BE (float64BitsOf (f64vec4_2 v)) ++ octets64BE (float64BitsOf (f64vec4_3 v))
  end.
