Example VUs -- post-english changes

Author: ShabbyX

chapters/clears.adoc

@@ -51,8 +51,8 @@ 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
+    codified-vu
+    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
@@ -67,38 +67,36 @@ endif::VK_VERSION_1_1,VK_KHR_sampler_ycbcr_conversion[]
     ranges of pname:image specified in pname:pRanges at the time this
     command is executed on a sname:VkDevice
   * [[VUID-vkCmdClearColorImage-imageLayout-01394]]
-    pname:imageLayout must: be
-ifdef::VK_KHR_shared_presentable_image[]
-    ename:VK_IMAGE_LAYOUT_SHARED_PRESENT_KHR,
-endif::VK_KHR_shared_presentable_image[]
-    ename:VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL or
-    ename:VK_IMAGE_LAYOUT_GENERAL
+    codified-vu
+    require(imageLayout == VK_IMAGE_LAYOUT_TRANSFER_DST_OPTIMAL or
+        imageLayout == VK_IMAGE_LAYOUT_GENERAL or
+        imageLayout == VK_IMAGE_LAYOUT_SHARED_PRESENT_KHR)
   * [[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
+    codified-vu
+    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
+    codified-vu
+    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
+    codified-vu
+    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
+    codified-vu
+    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
+    codified-vu
+    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

@@ -14,9 +14,11 @@
 //    corresponding to the offset and extent of the copy.
 
   * [[VUID-{refpage}-{imageparam}-07979]]
-    If pname:{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`
+    codified-vu
+    if macro(imageparam).create_info().imageType == VK_IMAGE_TYPE_1D:
+      for region in pRegions:
+        require(region.macro(imageoffset).y == 0)
+        require(region.macro(imageextent).height == 1)
   * [[VUID-{refpage}-{imageoffset}-09104]]
     For each element of pname:pRegions, pname:{imageoffset}.z and
     [eq]#(pname:{imageextent}.depth {plus} pname:{imageoffset}.z)# must:

chapters/descriptorsets.adoc

@@ -608,16 +608,12 @@ endif::VK_VERSION_1_4,VK_KHR_push_descriptor[]
 .Valid Usage
 ****
   * [[VUID-VkDescriptorSetLayoutCreateInfo-binding-00279]]
-ifdef::VK_NV_per_stage_descriptor_set[]
-    If the <<features-perStageDescriptorSet, pname:perStageDescriptorSet>>
-    feature is not enabled, or pname:flags does not contain
-    ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PER_STAGE_BIT_NV, then the
-endif::VK_NV_per_stage_descriptor_set[]
-ifndef::VK_NV_per_stage_descriptor_set[]
-    The
-endif::VK_NV_per_stage_descriptor_set[]
-    slink:VkDescriptorSetLayoutBinding::pname:binding members of the
-    elements of the pname:pBindings array must: each have different values
+    codified-vu
+    if not is_feature_enabled(perStageDescriptorSet) and not flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PER_STAGE_BIT_NV):
+      for binding in pBindings:
+        for binding2 in pBindings:
+          if array_index(binding2) != array_index(binding):
+            require(binding.binding != binding2.binding)
 ifdef::VK_VERSION_1_4[]
   * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-10354]]
     If pname:flags contains
@@ -629,17 +625,17 @@ endif::VK_KHR_push_descriptor[]
 endif::VK_VERSION_1_4[]
 ifdef::VK_VERSION_1_4,VK_KHR_push_descriptor[]
   * [[VUID-VkDescriptorSetLayoutCreateInfo-flags-00280]]
-    If pname:flags contains
-    ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT, 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
+    codified-vu
+    if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT):
+      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, then all
-    elements of pname:pBindings must: not have a pname:descriptorType of
-    ename:VK_DESCRIPTOR_TYPE_INLINE_UNIFORM_BLOCK
+    codified-vu
+    if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT):
+      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
@@ -648,22 +644,24 @@ endif::VK_VERSION_1_3,VK_EXT_inline_uniform_block[]
     slink:VkPhysicalDevicePushDescriptorProperties::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, pname:flags
-    must: not contain
-    ename:VK_DESCRIPTOR_SET_LAYOUT_CREATE_HOST_ONLY_POOL_BIT_EXT
+    codified-vu
+    if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT):
+      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,
-    pname:pBindings must: not have a pname:descriptorType of
-    ename:VK_DESCRIPTOR_TYPE_MUTABLE_EXT
+    codified-vu
+    if flags.has_bit(VK_DESCRIPTOR_SET_LAYOUT_CREATE_PUSH_DESCRIPTOR_BIT):
+      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_VERSION_1_4,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
+    codified-vu
+    if has_pnext(VkDescriptorSetLayoutBindingFlagsCreateInfo):
+      bindingFlagsCreateInfo = pnext(VkDescriptorSetLayoutBindingFlagsCreateInfo)
+      for bindingFlags in bindingFlagsCreateInfo.pBindingFlags:
+        if bindingFlags.has_bit(VK_DESCRIPTOR_BINDING_UPDATE_AFTER_BIND_BIT):
+          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
@@ -679,10 +677,12 @@ 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 the pname:pNext chain must:
-    include a slink:VkMutableDescriptorTypeCreateInfoEXT structure, and
-    pname:mutableDescriptorTypeListCount must: be greater than i
+    codified-vu
+    for binding in pBindings:
+      if binding.descriptorType == VK_DESCRIPTOR_TYPE_MUTABLE_EXT:
+        require(has_pnext(VkMutableDescriptorTypeCreateInfoEXT))
+        mutableCount = pnext(VkMutableDescriptorTypeCreateInfoEXT).mutableDescriptorTypeListCount
+        require(mutableCount > array_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

@@ -1972,13 +1972,14 @@ include::{generated}/api/structs/VkDeviceCreateInfo.adoc[]
 .Valid Usage
 ****
   * [[VUID-VkDeviceCreateInfo-queueFamilyIndex-02802]]
-    The pname:queueFamilyIndex member of each element of
-    pname:pQueueCreateInfos must: be unique within pname:pQueueCreateInfos
-ifdef::VK_VERSION_1_1[]
-    , 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
-endif::VK_VERSION_1_1[]
+    codified-vu
+    for queue in pQueueCreateInfos:
+      for queue2 in pQueueCreateInfos:
+        if array_index(queue2) != array_index(queue):
+          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)
 ifdef::VK_VERSION_1_1[]
   * [[VUID-VkDeviceCreateInfo-pQueueCreateInfos-06755]]
     If multiple elements of pname:pQueueCreateInfos share the same

chapters/pipelines.adoc

@@ -284,23 +284,23 @@ include::{chapters}/commonvalidity/no_dynamic_allocations_common.adoc[]
     ename:VK_QUEUE_COMPUTE_BIT capability
 ifndef::VKSC_VERSION_1_0[]
   * [[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
+    codified-vu
+    for info in pCreateInfos:
+      if (info.flags.has_bit(VK_PIPELINE_CREATE_DERIVATIVE_BIT) and
+          info.basePipelineIndex != -1):
+        require(info.basePipelineIndex < array_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
+    codified-vu
+    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))
 endif::VKSC_VERSION_1_0[]
 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>>
+    codified-vu
+    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[]
 include::{chapters}/commonvalidity/memory_reservation_request_count_common.adoc[]
 include::{chapters}/commonvalidity/pipeline_create_common.adoc[]

chapters/renderpass.adoc

@@ -405,13 +405,13 @@ 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
+    codified-vu
+    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