1921def softmaxSM86BuildValidated =
1922 (lambda unrestricted variant : (family SoftmaxSM86Variant) .
1923 (lambda unrestricted program : (family SM86Program) .
1924 (app
1925 (lambda unrestricted observedInstructions : Nat .
1926 (nat-eliminate
1927 (lambda unrestricted instructionCountExact : Nat . (family SoftmaxSM86BuildResult))
1928 (constructor
1929 SoftmaxSM86BuildResult
1930 SoftmaxSM86ContractFailed
1931 (constructor SoftmaxSM86FailureCode SoftmaxSM86InstructionCountMismatch)
1932 (softmaxSM86EmptyTelemetry variant observedInstructions))
1933 (lambda unrestricted instructionPredecessor : Nat .
1934 (lambda unrestricted instructionInduction : (family SoftmaxSM86BuildResult) .
1935 (app
1936 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
1937 (eliminate
1938 SM86ProgramEncodingResult
1939 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1940 (family SoftmaxSM86BuildResult))
1941 encoding
1942 (branch
1943 SM86ProgramEncodingSucceeded
1944 bytes
1945 encodingTelemetry
1946 .
1947 (eliminate
1948 SM86ProgramEncodingTelemetry
1949 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1950 (family SoftmaxSM86BuildResult))
1951 encodingTelemetry
1952 (branch
1953 SM86ProgramEncodingTelemetryValue
1954 encodedInstructions
1955 encodedBytes
1956 encodingFields
1957 encodingBits
1958 highestEncodedBit
1959 .
1960 (app
1961 (lambda unrestricted telemetry : (family SoftmaxSM86Telemetry) .
1962 (nat-eliminate
1963 (lambda unrestricted byteCountExact : Nat .
1964 (family SoftmaxSM86BuildResult))
1965 (constructor
1966 SoftmaxSM86BuildResult
1967 SoftmaxSM86ContractFailed
1968 (constructor
1969 SoftmaxSM86FailureCode
1970 SoftmaxSM86EncodedByteCountMismatch)
1971 telemetry)
1972 (lambda unrestricted bytePredecessor : Nat .
1973 (lambda unrestricted byteInduction : (family SoftmaxSM86BuildResult) .
1974 (app
1975 (lambda unrestricted identityResult : (family SHA256HexResult) .
1976 (eliminate
1977 SHA256HexResult
1978 (lambda unrestricted current : (family SHA256HexResult) .
1979 (family SoftmaxSM86BuildResult))
1980 identityResult
1981 (branch
1982 SHA256HexSucceeded
1983 identity
1984 identityTelemetry
1985 .
1986 (app
1987 (lambda unrestricted identityTelemetryValue : (family SoftmaxSM86Telemetry) .
1988 (nat-eliminate
1989 (lambda unrestricted identityLengthExact : Nat .
1990 (family SoftmaxSM86BuildResult))
1991 (constructor
1992 SoftmaxSM86BuildResult
1993 SoftmaxSM86ImageIdentityFailed
1994 (constructor
1995 SoftmaxSM86FailureCode
1996 SoftmaxSM86IdentityLengthInvalid)
1997 identityResult
1998 identityTelemetryValue)
1999 (lambda unrestricted identityLengthPredecessor : Nat .
2000 (lambda unrestricted identityLengthInduction : (family SoftmaxSM86BuildResult) .
2001 (nat-eliminate
2002 (lambda unrestricted identityExact : Nat .
2003 (family SoftmaxSM86BuildResult))
2004 (constructor
2005 SoftmaxSM86BuildResult
2006 SoftmaxSM86ImageIdentityFailed
2007 (constructor
2008 SoftmaxSM86FailureCode
2009 SoftmaxSM86IdentityMismatch)
2010 identityResult
2011 identityTelemetryValue)
2012 (lambda unrestricted identityPredecessor : Nat .
2013 (lambda unrestricted identityInduction : (family SoftmaxSM86BuildResult) .
2014 (constructor
2015 SoftmaxSM86BuildResult
2016 SoftmaxSM86BuildSucceeded
2017 bytes
2018 identity
2019 encodingTelemetry
2020 identityTelemetry
2021 identityTelemetryValue)))
2022 (bytes-equal
2023 identity
2024 (softmaxSM86ExpectedSHA256For variant)))))
2025 (naturalEqual (bytes-length identity) softmaxSM86N64)))
2026 (softmaxSM86TelemetryFor
2027 variant
2028 observedInstructions
2029 (bytes-length bytes)
2030 encodingFields
2031 encodingBits
2032 highestEncodedBit
2033 (bytes-length bytes)
2034 (bytes-length identity))))
2035 (branch
2036 SHA256HexFailed
2037 error
2038 ordinal
2039 identityTelemetry
2040 .
2041 (constructor
2042 SoftmaxSM86BuildResult
2043 SoftmaxSM86ImageIdentityFailed
2044 (constructor
2045 SoftmaxSM86FailureCode
2046 SoftmaxSM86IdentityFailed)
2047 identityResult
2048 (softmaxSM86TelemetryFor
2049 variant
2050 observedInstructions
2051 (bytes-length bytes)
2052 encodingFields
2053 encodingBits
2054 highestEncodedBit
2055 (bytes-length bytes)
2056 zero)))))
2057 (sha256Hex bytes))))
2058 (naturalEqual
2059 (bytes-length bytes)
2060 (softmaxSM86ExpectedBytesFor variant))))
2061 (softmaxSM86TelemetryFor
2062 variant
2063 observedInstructions
2064 (bytes-length bytes)
2065 encodingFields
2066 encodingBits
2067 highestEncodedBit
2068 zero
2069 zero)))))
2070 (branch
2071 SM86ProgramEncodingFailed
2072 instructionIndex
2073 failure
2074 encodingTelemetry
2075 .
2076 (constructor
2077 SoftmaxSM86BuildResult
2078 SoftmaxSM86ImageEncodingFailed
2079 (constructor SoftmaxSM86FailureCode SoftmaxSM86EncodingFailed)
2080 encoding
2081 (softmaxSM86EmptyTelemetry variant observedInstructions)))))
2082 (sm86EncodeProgram program))))
2083 (naturalEqual observedInstructions (softmaxSM86ExpectedInstructionsFor variant))))
2084 (sm86ProgramCount program))))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.