DO NOT MERGE: Example codified VUs

chapters/clears.adoc

@@ -51,8 +51,7 @@ ifdef::VK_VERSION_1_1,VK_KHR_maintenance1[]
  must: contain ename:VK_FORMAT_FEATURE_TRANSFER_DST_BIT
 endif::VK_VERSION_1_1,VK_KHR_maintenance1[]
  * [[VUID-vkCmdClearColorImage-image-00002]]
- pname:image must: have been created with
- ename:VK_IMAGE_USAGE_TRANSFER_DST_BIT usage flag
+ require(image.create_info().usage.has_bit(VK_IMAGE_USAGE_TRANSFER_DST_BIT))
 ifdef::VK_VERSION_1_1,VK_KHR_sampler_ycbcr_conversion[]
  * [[VUID-vkCmdClearColorImage-image-01545]]
  pname:image must: not use any of the
@@ -68,41 +67,36 @@ endif::VK_VERSION_1_1,VK_KHR_sampler_ycbcr_conversion[]
  command is executed on a sname:VkDevice
 ifndef::VK_KHR_shared_presentable_image[]
  * [[VUID-vkCmdClearColorImage-imageLayout-00005]]
- pname:imageLayout must: be ename:VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL or
- ename:VK_IMAGE_LAYOUT_GENERAL
+ require(imageLayout == VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL or
+  imageLayout == VK_IMAGE_LAYOUT_GENERAL)
 endif::VK_KHR_shared_presentable_image[]
 ifdef::VK_KHR_shared_presentable_image[]
  * [[VUID-vkCmdClearColorImage-imageLayout-01394]]
- pname:imageLayout must: be ename:VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL,
- ename:VK_IMAGE_LAYOUT_GENERAL, or
- ename:VK_IMAGE_LAYOUT_SHARED_PRESENT_KHR
+ require(imageLayout == VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL or
+  imageLayout == VK_IMAGE_LAYOUT_GENERAL or
+  imageLayout == VK_IMAGE_LAYOUT_SHARED_PRESENT_KHR)
 endif::VK_KHR_shared_presentable_image[]
  * [[VUID-vkCmdClearColorImage-aspectMask-02498]]
- The slink:VkImageSubresourceRange::pname:aspectMask members of the
- elements of the pname:pRanges array must: each only include
- ename:VK_IMAGE_ASPECT_COLOR_BIT
+ for range in pRanges:
+ require(range.aspectMask == VK_IMAGE_ASPECT_COLOR_BIT)
  * [[VUID-vkCmdClearColorImage-baseMipLevel-01470]]
- The slink:VkImageSubresourceRange::pname:baseMipLevel members of the
- elements of the pname:pRanges array must: each be less than the
- pname:mipLevels specified in slink:VkImageCreateInfo when pname:image
- was created
+ mipLevels = image.create_info().mipLevels
+ for range in pRanges:
+ require(range.baseMipLevel < mipLevels)
  * [[VUID-vkCmdClearColorImage-pRanges-01692]]
- For each slink:VkImageSubresourceRange element of pname:pRanges, if the
- pname:levelCount member is not ename:VK_REMAINING_MIP_LEVELS, then
- [eq]#pname:baseMipLevel {plus} pname:levelCount# must: be less than or
- equal to the pname:mipLevels specified in slink:VkImageCreateInfo when
- pname:image was created
+ mipLevels = image.create_info().mipLevels
+ for range in pRanges:
+ if range.levelCount != VK_REMAINING_MIP_LEVELS:
+ require(range.baseMipLevel + range.levelCount <= mipLevels)
  * [[VUID-vkCmdClearColorImage-baseArrayLayer-01472]]
- The slink:VkImageSubresourceRange::pname:baseArrayLayer members of the
- elements of the pname:pRanges array must: each be less than the
- pname:arrayLayers specified in slink:VkImageCreateInfo when pname:image
- was created
+ arrayLayers = image.create_info().arrayLayers
+ for range in pRanges:
+ require(range.baseArrayLayer < arrayLayers)
  * [[VUID-vkCmdClearColorImage-pRanges-01693]]
- For each slink:VkImageSubresourceRange element of pname:pRanges, if the
- pname:layerCount member is not ename:VK_REMAINING_ARRAY_LAYERS, then
- [eq]#pname:baseArrayLayer {plus} pname:layerCount# must: be less than or
- equal to the pname:arrayLayers specified in slink:VkImageCreateInfo when
- pname:image was created
+ arrayLayers = image.create_info().arrayLayers
+ for range in pRanges:
+ if range.layerCount != VK_REMAINING_ARRAY_LAYERS:
+ require(range.baseArrayLayer + range.layerCount <= arrayLayers)
  * [[VUID-vkCmdClearColorImage-image-00007]]
  pname:image must: not have a compressed or depth/stencil format
  * [[VUID-vkCmdClearColorImage-pColor-04961]]

chapters/commonvalidity/copy_bufferimage_to_imagebuffer_common.adoc

@@ -9,9 +9,10 @@
 // destination image.
 
  * [[VUID-{refpage}-srcImage-00199]]
- If {imageparam} is of type ename:VK_IMAGE_TYPE_1D, then for each element
- of pname:pRegions, pname:imageOffset.y must: be `0` and
- pname:imageExtent.height must: be `1`
+ if macro(imageparam).create_info().imageType == VK_IMAGE_TYPE_1D:
+ for region in pRegions:
+ require(region.imageOffset.y == 0)
+ require(region.imageExtent.height == 1)
  * [[VUID-{refpage}-imageOffset-00200]]
  For each element of pname:pRegions, pname:imageOffset.z and
  [eq]#(pname:imageExtent.depth {plus} pname:imageOffset.z)# must: both be

chapters/descriptorsets.adoc

@@ -579,21 +579,22 @@ endif::VK_KHR_push_descriptor[]
 .Valid Usage
 ****
  * [[VUID-VkDescriptorSetLayoutCreateInfo-binding-00279]]
- The slink:VkDescriptorSetLayoutBinding::pname:binding members of the
- elements of the pname:pBindings array must: each have different values
+ for binding in pBindings:
+ for binding2 in pBindings:
+ if loop_index(binding2) >= loop_index(binding):
+ break
+ require(binding.binding != binding2.binding)
 ifdef::VK_KHR_push_descriptor[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-00280]]
- If pname:flags contains
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR, then all
- elements of pname:pBindings must: not have a pname:descriptorType of
- ename:VK_DESCRIPTOR_TYPE_UNIFORM_BUFFER_DYNAMIC or
- ename:VK_DESCRIPTOR_TYPE_STORAGE_BUFFER_DYNAMIC
+ if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR):
+ for binding in pBindings:
+ require(binding.descriptorType != VK_DESCRIPTOR_TYPE_UNIFORM_BUFFER_DYNAMIC and
+ binding.descriptorType != VK_DESCRIPTOR_TYPE_STORAGE_BUFFER_DYNAMIC)
 ifdef::VK_VERSION_1_3,VK_EXT_inline_uniform_block[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-02208]]
- If pname:flags contains
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR, then all
- elements of pname:pBindings must: not have a pname:descriptorType of
- ename:VK_DESCRIPTOR_TYPE_INLINE_UNIFORM_BLOCK
+ if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR):
+ for binding in pBindings:
+ require(binding.descriptorType != VK_DESCRIPTOR_TYPE_INLINE_UNIFORM_BLOCK)
 endif::VK_VERSION_1_3,VK_EXT_inline_uniform_block[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-00281]]
  If pname:flags contains
@@ -602,22 +603,25 @@ endif::VK_VERSION_1_3,VK_EXT_inline_uniform_block[]
  slink:VkPhysicalDevicePushDescriptorPropertiesKHR::pname:maxPushDescriptors
 ifdef::VK_EXT_mutable_descriptor_type,VK_VALVE_mutable_descriptor_type[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-04590]]
- If pname:flags contains
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR,
- pname:flags must: not contain
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_HOST_ONLY_POOL_BIT_EXT
+ if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR):
+ require(not flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_HOST_ONLY_POOL_BIT_EXT))
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-04591]]
- If pname:flags contains
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR,
- pname:pBindings must: not have a pname:descriptorType of
- ename:VK_DESCRIPTOR_TYPE_MUTABLE_EXT
+ if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT_KHR):
+ for binding in pBindings:
+ require(binding.descriptorType != VK_DESCRIPTOR_TYPE_MUTABLE_EXT)
 endif::VK_EXT_mutable_descriptor_type,VK_VALVE_mutable_descriptor_type[]
 endif::VK_KHR_push_descriptor[]
 ifdef::VK_VERSION_1_2,VK_EXT_descriptor_indexing[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-03000]]
- If any binding has the ename:VK_DESCRIPTOR_BINDING_UPDATE_AFTER_BIND_BIT
- bit set, pname:flags must: include
- ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_UPDATE_AFTER_BIND_POOL_BIT
+ if has_pnext(VkDescriptorSetLayoutBindingFlagsCreateInfoEXT):
+ bindingFlagsCreateInfo = pnext(VkDescriptorSetLayoutBindingFlagsCreateInfoEXT)
+ hasUpdateAfterBind = False
+ for bindingFlags in bindingFlagsCreateInfo.pBindingFlags:
+ if bindingFlags.has_bit(VK_DESCRIPTOR_BINDING_UPDATE_AFTER_BIND_BIT):
+ hasUpdateAfterBind = True
+ break
+ if hasUpdateAfterBind:
+ require(flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_UPDATE_AFTER_BIND_POOL_BIT))
  * [[VUID-VkDescriptorSetLayoutCreateInfo-descriptorType-03001]]
  If any binding has the ename:VK_DESCRIPTOR_BINDING_UPDATE_AFTER_BIND_BIT
  bit set, then all bindings must: not have pname:descriptorType of
@@ -633,11 +637,11 @@ endif::VK_EXT_mutable_descriptor_type,VK_VALVE_mutable_descriptor_type[]
 endif::VK_VERSION_1_2,VK_EXT_descriptor_indexing[]
 ifdef::VK_EXT_mutable_descriptor_type,VK_VALVE_mutable_descriptor_type[]
  * [[VUID-VkDescriptorSetLayoutCreateInfo-pBindings-07303]]
- If any element pname:pBindings[i] has a pname:descriptorType of
- ename:VK_DESCRIPTOR_TYPE_MUTABLE_EXT, then a
- slink:VkMutableDescriptorTypeCreateInfoEXT must: be present in the
- pname:pNext chain, and pname:mutableDescriptorTypeListCount must: be
- greater than i
+ for binding in pBindings:
+  if binding.descriptorType == VK_DESCRIPTOR_TYPE_MUTABLE_EXT:
+  require(has_pnext(VkMutableDescriptorTypeCreateInfoEXT))
+  mutableCount = pnext(VkMutableDescriptorTypeCreateInfoEXT).mutableDescriptorTypeListCount
+  require(mutableCount > loop_index(binding))
  * [[VUID-VkDescriptorSetLayoutCreateInfo-descriptorType-04594]]
  If a binding has a pname:descriptorType value of
  ename:VK_DESCRIPTOR_TYPE_MUTABLE_EXT, then sname:pImmutableSamplers

chapters/devsandqueues.adoc

@@ -1588,16 +1588,22 @@ include::{generated}/api/structs/VkDeviceCreateInfo.adoc[]
 ****
 ifndef::VK_VERSION_1_1[]
  * [[VUID-VkDeviceCreateInfo-queueFamilyIndex-00372]]
- The pname:queueFamilyIndex member of each element of
- pname:pQueueCreateInfos must: be unique within pname:pQueueCreateInfos
+ for queue in pQueueCreateInfos:
+ for queue2 in pQueueCreateInfos:
+ if loop_index(queue2) >= loop_index(queue):
+ break
+ require(queue.queueFamilyIndex != queue2.queueFamilyIndex)
 endif::VK_VERSION_1_1[]
 ifdef::VK_VERSION_1_1[]
  * [[VUID-VkDeviceCreateInfo-queueFamilyIndex-02802]]
- The pname:queueFamilyIndex member of each element of
- pname:pQueueCreateInfos must: be unique within pname:pQueueCreateInfos,
- except that two members can share the same pname:queueFamilyIndex if one
- describes protected-capable queues and one describes queues that are not
- protected-capable
+ for queue in pQueueCreateInfos:
+ for queue2 in pQueueCreateInfos:
+ if loop_index(queue2) >= loop_index(queue):
+ break
+ protected = queue.flags.has_bit(VK_DEVICE_QUEUE_CREATE_PROTECTED_BIT)
+ protected2 = queue2.flags.has_bit(VK_DEVICE_QUEUE_CREATE_PROTECTED_BIT)
+ require(queue.queueFamilyIndex != queue2.queueFamilyIndex or
+ protected != protected2)
  * [[VUID-VkDeviceCreateInfo-pQueueCreateInfos-06755]]
  If multiple elements of pname:pQueueCreateInfos share the same
  pname:queueFamilyIndex, the sum of their pname:queueCount members must:

chapters/pipelines.adoc

@@ -176,22 +176,17 @@ endif::editing-notes[]
 .Valid Usage
 ****
  * [[VUID-vkCreateComputePipelines-flags-00695]]
- If the pname:flags member of any element of pname:pCreateInfos contains
- the ename:VK_PIPELINE_CREATE_DERIVATIVE_BIT flag, and the
- pname:basePipelineIndex member of that same element is not `-1`,
- pname:basePipelineIndex must: be less than the index into
- pname:pCreateInfos that corresponds to that element
+ for info in pCreateInfos:
+ if info.flags.has_bit(VK_PIPELINE_CREATE_DERIVATIVE_BIT) and info.basePipelineIndex != -1:
+ require(info.basePipelineIndex < loop_index(info))
  * [[VUID-vkCreateComputePipelines-flags-00696]]
- If the pname:flags member of any element of pname:pCreateInfos contains
- the ename:VK_PIPELINE_CREATE_DERIVATIVE_BIT flag, the base pipeline
- must: have been created with the
- ename:VK_PIPELINE_CREATE_ALLOW_DERIVATIVES_BIT flag set
+ for info in pCreateInfos:
+ if info.flags.has_bit(VK_PIPELINE_CREATE_DERIVATIVE_BIT) and info.basePipelineIndex != -1:
+ require(pCreateInfos[info.basePipelineIndex].flags.has_bit(VK_PIPELINE_CREATE_ALLOW_DERIVATIVES_BIT))
 ifdef::VK_VERSION_1_3,VK_EXT_pipeline_creation_cache_control[]
  * [[VUID-vkCreateComputePipelines-pipelineCache-02873]]
- If pname:pipelineCache was created with
- ename:VK_PIPELINE_CACHE_CREATE_EXTERNALLY_SYNCHRONIZED_BIT, host access
- to pname:pipelineCache must: be
- <<fundamentals-threadingbehavior,externally synchronized>>
+ if pipelineCache.create_info().flags.has_bit(VK_PIPELINE_CACHE_CREATE_EXTERNALLY_SYNCHRONIZED_BIT):
+ require(externally_synchronized(pipelineCache))
 endif::VK_VERSION_1_3,VK_EXT_pipeline_creation_cache_control[]
 ****
 

chapters/renderpass.adoc

@@ -298,13 +298,12 @@ ifdef::VK_KHR_maintenance2,VK_VERSION_1_1[]
  not be ename:VK_IMAGE_LAYOUT_DEPTH_READ_ONLY_STENCIL_ATTACHMENT_OPTIMAL
  or ename:VK_IMAGE_LAYOUT_DEPTH_ATTACHMENT_STENCIL_READ_ONLY_OPTIMAL
  * [[VUID-VkRenderingInfo-colorAttachmentCount-06097]]
- If pname:colorAttachmentCount is not `0` and the pname:imageView member
- of an element of pname:pColorAttachments is not dlink:VK_NULL_HANDLE, if
- the pname:resolveMode member of that element of pname:pColorAttachments
- is not ename:VK_RESOLVE_MODE_NONE, its pname:resolveImageLayout member
- must: not be
- ename:VK_IMAGE_LAYOUT_DEPTH_READ_ONLY_STENCIL_ATTACHMENT_OPTIMAL or
- ename:VK_IMAGE_LAYOUT_DEPTH_ATTACHMENT_STENCIL_READ_ONLY_OPTIMAL
+ for attachment in pColorAttachments:
+ if (attachment.imageView != VK_NULL_HANDLE and
+ attachment.resolveMode != VK_RESOLVE_MODE_NONE):
+ resolveLayout = attachment.resolveImageLayout
+ require(resolveLayout != VK_IMAGE_LAYOUT_DEPTH_READ_ONLY_STENCIL_ATTACHMENT_OPTIMAL and
+ resolveLayout != VK_IMAGE_LAYOUT_DEPTH_ATTACHMENT_STENCIL_READ_ONLY_OPTIMAL)
  * [[VUID-VkRenderingInfo-pDepthAttachment-06098]]
  If pname:pDepthAttachment is not `NULL`,
  pname:pDepthAttachment->imageView is not dlink:VK_NULL_HANDLE, and