Decodes and validates an artifact after the native hasher has supplied all
five observations. No bytes reach GPU submission through a failed result.
744def nativePhysicalEmbeddedLoad =
745 (lambda unrestricted artifactBytes : Bytes .
746 (lambda unrestricted observed : (family NativePhysicalEmbeddedObservedDigests) .
747 (let unrestricted artifactLength = (bytes-length artifactBytes) in
748 (let unrestricted footerOffset =
749 (naturalSaturatingSubtract artifactLength nativePhysicalEmbeddedFooterLength)
750 in
751 (let unrestricted footerBytes =
752 (nativePhysicalEmbeddedSliceOrEmpty
753 artifactBytes
754 footerOffset
755 nativePhysicalEmbeddedFooterLength)
756 in
757 (let unrestricted manifestLength =
758 nativePhysicalEmbeddedManifestLength
759 in
760 (let unrestricted manifestOffset =
761 (naturalSaturatingSubtract footerOffset manifestLength)
762 in
763 (let unrestricted manifestBytes =
764 (nativePhysicalEmbeddedSliceOrEmpty
765 artifactBytes
766 manifestOffset
767 manifestLength)
768 in
769 (let unrestricted footerValid =
770 (naturalAnd
771 (naturalLessOrEqual nativePhysicalEmbeddedFooterLength artifactLength)
772 (naturalAnd
773 (bytes-equal
774 (nativePhysicalEmbeddedSliceOrEmpty
775 footerBytes
776 zero
777 (byte-to-nat (byte 8)))
778 nativePhysicalEmbeddedFooterMagic)
779 (naturalAnd
780 (bytes-equal
781 (nativePhysicalEmbeddedSliceOrEmpty
782 footerBytes
783 (byte-to-nat (byte 8))
784 (byte-to-nat (byte 4)))
785 (nativePhysicalEmbeddedWord32Bytes manifestOffset))
786 (bytes-equal
787 (nativePhysicalEmbeddedSliceOrEmpty
788 footerBytes
789 (byte-to-nat (byte 12))
790 (byte-to-nat (byte 4)))
791 (nativePhysicalEmbeddedWord32Bytes manifestLength)))))
792 in
793 (let unrestricted manifestValid =
794 (naturalAnd
795 (naturalEqual
796 (bytes-length manifestBytes)
797 nativePhysicalEmbeddedManifestLength)
798 (naturalAnd
799 (bytes-equal
800 (nativePhysicalEmbeddedSliceOrEmpty
801 manifestBytes
802 zero
803 (byte-to-nat (byte 8)))
804 nativePhysicalEmbeddedManifestMagic)
805 (naturalEqual
806 (nativePhysicalEmbeddedWord32At
807 manifestBytes
808 (byte-to-nat (byte 8)))
809 nativePhysicalEmbeddedVersion)))
810 in
811 (let unrestricted host =
812 (nativePhysicalEmbeddedDescriptorAt
813 manifestBytes
814 (byte-to-nat (byte 12))
815 (constructor
816 NativePhysicalEmbeddedComponentKind
817 NativePhysicalEmbeddedHostELF))
818 in
819 (let unrestricted program =
820 (nativePhysicalEmbeddedDescriptorAt
821 manifestBytes
822 (byte-to-nat (byte 120))
823 (constructor
824 NativePhysicalEmbeddedComponentKind
825 NativePhysicalEmbeddedProgramTable))
826 in
827 (let unrestricted qmd =
828 (nativePhysicalEmbeddedDescriptorAt
829 manifestBytes
830 (byte-to-nat (byte 228))
831 (constructor
832 NativePhysicalEmbeddedComponentKind
833 NativePhysicalEmbeddedQMDTable))
834 in
835 (let unrestricted pushbuffer =
836 (nativePhysicalEmbeddedDescriptorAt
837 manifestBytes
838 336
839 (constructor
840 NativePhysicalEmbeddedComponentKind
841 NativePhysicalEmbeddedPushbuffer))
842 in
843 (let unrestricted gpfifo =
844 (nativePhysicalEmbeddedDescriptorAt
845 manifestBytes
846 444
847 (constructor
848 NativePhysicalEmbeddedComponentKind
849 NativePhysicalEmbeddedGPFIFO))
850 in
851 (let unrestricted tagsValid =
852 (naturalAnd
853 (naturalEqual
854 (nativePhysicalEmbeddedDescriptorTagAt
855 manifestBytes
856 (byte-to-nat (byte 12)))
857 (succ zero))
858 (naturalAnd
859 (naturalEqual
860 (nativePhysicalEmbeddedDescriptorTagAt
861 manifestBytes
862 (byte-to-nat (byte 120)))
863 (byte-to-nat (byte 2)))
864 (naturalAnd
865 (naturalEqual
866 (nativePhysicalEmbeddedDescriptorTagAt
867 manifestBytes
868 (byte-to-nat (byte 228)))
869 (byte-to-nat (byte 3)))
870 (naturalAnd
871 (naturalEqual
872 (nativePhysicalEmbeddedDescriptorTagAt
873 manifestBytes
874 336)
875 (byte-to-nat (byte 4)))
876 (naturalEqual
877 (nativePhysicalEmbeddedDescriptorTagAt
878 manifestBytes
879 444)
880 (byte-to-nat (byte 5)))))))
881 in
882 (let unrestricted layoutValid =
883 (nativePhysicalEmbeddedLayoutValid
884 host
885 program
886 qmd
887 pushbuffer
888 gpfifo
889 manifestOffset)
890 in
891 (let unrestricted hashesValid =
892 (nativePhysicalEmbeddedHashesValid
893 host
894 program
895 qmd
896 pushbuffer
897 gpfifo
898 observed)
899 in
900 (let unrestricted allValid =
901 (naturalAnd
902 footerValid
903 (naturalAnd
904 manifestValid
905 (naturalAnd tagsValid (naturalAnd layoutValid hashesValid))))
906 in
907 (nat-eliminate
908 (lambda unrestricted current : Nat .
909 (family NativePhysicalEmbeddedLoadResult))
910 (constructor
911 NativePhysicalEmbeddedLoadResult
912 NativePhysicalEmbeddedLoadFailed
913 (constructor
914 NativePhysicalEmbeddedErrorCode
915 NativePhysicalEmbeddedManifestInvalid))
916 (lambda unrestricted validPredecessor : Nat .
917 (lambda unrestricted validInduction :
918 (family NativePhysicalEmbeddedLoadResult) .
919 (let unrestricted hostBytes =
920 (nativePhysicalEmbeddedSliceOrEmpty
921 artifactBytes
922 (nativePhysicalEmbeddedDescriptorOffsetValue host)
923 (nativePhysicalEmbeddedDescriptorLengthValue host))
924 in
925 (let unrestricted programBytes =
926 (nativePhysicalEmbeddedSliceOrEmpty
927 artifactBytes
928 (nativePhysicalEmbeddedDescriptorOffsetValue program)
929 (nativePhysicalEmbeddedDescriptorLengthValue program))
930 in
931 (let unrestricted qmdBytes =
932 (nativePhysicalEmbeddedSliceOrEmpty
933 artifactBytes
934 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
935 (nativePhysicalEmbeddedDescriptorLengthValue qmd))
936 in
937 (let unrestricted pushbufferBytes =
938 (nativePhysicalEmbeddedSliceOrEmpty
939 artifactBytes
940 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
941 (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer))
942 in
943 (let unrestricted gpfifoBytes =
944 (nativePhysicalEmbeddedSliceOrEmpty
945 artifactBytes
946 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
947 (nativePhysicalEmbeddedDescriptorLengthValue gpfifo))
948 in
949 (let unrestricted manifest =
950 (constructor
951 NativePhysicalEmbeddedManifest
952 NativePhysicalEmbeddedManifestValue
953 nativePhysicalEmbeddedVersion
954 host
955 program
956 qmd
957 pushbuffer
958 gpfifo
959 manifestBytes
960 manifestOffset
961 artifactLength)
962 in
963 (constructor
964 NativePhysicalEmbeddedLoadResult
965 NativePhysicalEmbeddedLoadSucceeded
966 (constructor
967 NativePhysicalEmbeddedArtifact
968 NativePhysicalEmbeddedArtifactValue
969 artifactBytes
970 manifest)
971 hostBytes
972 programBytes
973 qmdBytes
974 pushbufferBytes
975 gpfifoBytes)))))))))
976 allValid))))))))))))))))))))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.