Version-1 descriptors must be contiguous and end exactly at the manifest.
661def nativePhysicalEmbeddedLayoutValid =
662 (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) .
663 (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) .
664 (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) .
665 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) .
666 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) .
667 (lambda unrestricted manifestOffset : Nat .
668 (naturalAnd
669 (naturalNonzero (nativePhysicalEmbeddedDescriptorLengthValue host))
670 (naturalAnd
671 (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue host) zero)
672 (naturalAnd
673 (naturalEqual
674 (nativePhysicalEmbeddedDescriptorOffsetValue program)
675 (nativePhysicalEmbeddedDescriptorLengthValue host))
676 (naturalAnd
677 (naturalEqual
678 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
679 (naturalAdd
680 (nativePhysicalEmbeddedDescriptorOffsetValue program)
681 (nativePhysicalEmbeddedDescriptorLengthValue program)))
682 (naturalAnd
683 (naturalEqual
684 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
685 (naturalAdd
686 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
687 (nativePhysicalEmbeddedDescriptorLengthValue qmd)))
688 (naturalAnd
689 (naturalEqual
690 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
691 (naturalAdd
692 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
693 (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer)))
694 (naturalEqual
695 manifestOffset
696 (naturalAdd
697 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
698 (nativePhysicalEmbeddedDescriptorLengthValue gpfifo)))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.