897def reductionSM86Build =
898 (lambda unrestricted program : (family SM86Program) .
899 (lambda unrestricted expected : Nat .
900 (lambda unrestricted mismatchCode : (family ReductionSM86FailureCode) .
901 (lambda unrestricted makeTelemetry : (pi unrestricted observed : Nat . (family ReductionSM86Telemetry)) .
902 (app
903 (lambda unrestricted observed : Nat .
904 (app
905 (lambda unrestricted telemetry : (family ReductionSM86Telemetry) .
906 (nat-eliminate
907 (lambda unrestricted countMatched : Nat . (family ReductionSM86BuildResult))
908 (constructor
909 ReductionSM86BuildResult
910 ReductionSM86ContractFailed
911 mismatchCode
912 telemetry)
913 (lambda unrestricted matchedPredecessor : Nat .
914 (lambda unrestricted matchedInduction : (family ReductionSM86BuildResult) .
915 (app
916 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
917 (eliminate
918 SM86ProgramEncodingResult
919 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
920 (family ReductionSM86BuildResult))
921 encoding
922 (branch
923 SM86ProgramEncodingSucceeded
924 bytes
925 encodingTelemetry
926 .
927 (app
928 (lambda unrestricted identityResult : (family SHA256HexResult) .
929 (eliminate
930 SHA256HexResult
931 (lambda unrestricted current : (family SHA256HexResult) .
932 (family ReductionSM86BuildResult))
933 identityResult
934 (branch
935 SHA256HexSucceeded
936 identity
937 identityTelemetry
938 .
939 (nat-eliminate
940 (lambda unrestricted validIdentityLength : Nat .
941 (family ReductionSM86BuildResult))
942 (constructor
943 ReductionSM86BuildResult
944 ReductionSM86SnippetIdentityFailed
945 (constructor
946 ReductionSM86FailureCode
947 ReductionSM86IdentityLengthInvalid)
948 identityResult
949 telemetry)
950 (lambda unrestricted identityLengthPredecessor : Nat .
951 (lambda unrestricted identityLengthInduction : (family ReductionSM86BuildResult) .
952 (constructor
953 ReductionSM86BuildResult
954 ReductionSM86BuildSucceeded
955 bytes
956 identity
957 encodingTelemetry
958 identityTelemetry
959 telemetry)))
960 (naturalEqual
961 (bytes-length identity)
962 (byte-to-nat (byte 64)))))
963 (branch
964 SHA256HexFailed
965 error
966 ordinal
967 identityTelemetry
968 .
969 (constructor
970 ReductionSM86BuildResult
971 ReductionSM86SnippetIdentityFailed
972 (constructor
973 ReductionSM86FailureCode
974 ReductionSM86IdentityFailed)
975 identityResult
976 telemetry))))
977 (sha256Hex bytes)))
978 (branch
979 SM86ProgramEncodingFailed
980 instructionIndex
981 failure
982 encodingTelemetry
983 .
984 (constructor
985 ReductionSM86BuildResult
986 ReductionSM86SnippetEncodingFailed
987 (constructor ReductionSM86FailureCode ReductionSM86EncodingFailed)
988 encoding
989 telemetry))))
990 (sm86EncodeProgram program))))
991 (naturalEqual observed expected)))
992 (makeTelemetry observed)))
993 (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.