1979def checkpointValidateBlocks =
1980 (lambda unrestricted fields : (family CheckpointFields) .
1981 (eliminate
1982 CheckpointFields
1983 (lambda unrestricted current : (family CheckpointFields) .
1984 (pi unrestricted blocks : (family CheckpointBlocks) .
1985 (family CheckpointBlocksValidationResult)))
1986 fields
1987 (branch
1988 CheckpointFieldsEnd
1989 .
1990 (lambda unrestricted blocks : (family CheckpointBlocks) .
1991 (eliminate
1992 CheckpointBlocks
1993 (lambda unrestricted current : (family CheckpointBlocks) .
1994 (family CheckpointBlocksValidationResult))
1995 blocks
1996 (branch
1997 CheckpointBlocksEnd
1998 .
1999 (constructor
2000 CheckpointBlocksValidationResult
2001 CheckpointBlocksAccepted
2002 (constructor CheckpointTypedBlocks CheckpointTypedBlocksEnd)
2003 modelWord64Zero
2004 zero))
2005 (branch
2006 CheckpointBlocksNext
2007 head
2008 tail
2009 ih_tail
2010 .
2011 (constructor
2012 CheckpointBlocksValidationResult
2013 CheckpointBlocksRejected
2014 (checkpointSimpleFailure
2015 (constructor CheckpointErrorCode CheckpointFieldCountMismatch)
2016 zero)
2017 modelWord64Zero
2018 zero)))))
2019 (branch
2020 CheckpointFieldsNext
2021 field
2022 remainingFields
2023 ih_fields
2024 .
2025 (lambda unrestricted blocks : (family CheckpointBlocks) .
2026 (eliminate
2027 CheckpointBlocks
2028 (lambda unrestricted current : (family CheckpointBlocks) .
2029 (family CheckpointBlocksValidationResult))
2030 blocks
2031 (branch
2032 CheckpointBlocksEnd
2033 .
2034 (constructor
2035 CheckpointBlocksValidationResult
2036 CheckpointBlocksRejected
2037 (checkpointSimpleFailure
2038 (constructor CheckpointErrorCode CheckpointFieldCountMismatch)
2039 zero)
2040 modelWord64Zero
2041 zero))
2042 (branch
2043 CheckpointBlocksNext
2044 block
2045 remainingBlocks
2046 ih_blocks
2047 .
2048 (eliminate
2049 CheckpointField
2050 (lambda unrestricted current : (family CheckpointField) .
2051 (family CheckpointBlocksValidationResult))
2052 field
2053 (branch
2054 CheckpointFieldValue
2055 kind
2056 expectedName
2057 storageOffset
2058 streamOffset
2059 expectedLength
2060 elements
2061 domain
2062 initialization
2063 .
2064 (eliminate
2065 CheckpointBlock
2066 (lambda unrestricted current : (family CheckpointBlock) .
2067 (family CheckpointBlocksValidationResult))
2068 block
2069 (branch
2070 CheckpointBlockValue
2071 actualName
2072 payload
2073 .
2074 (nat-eliminate
2075 (lambda unrestricted nameMatched : Nat .
2076 (family CheckpointBlocksValidationResult))
2077 (constructor
2078 CheckpointBlocksValidationResult
2079 CheckpointBlocksRejected
2080 (checkpointFailure
2081 (constructor CheckpointErrorCode CheckpointFieldNameMismatch)
2082 zero
2083 expectedName
2084 actualName)
2085 modelWord64Zero
2086 zero)
2087 (lambda unrestricted namePredecessor : Nat .
2088 (lambda unrestricted nameInduction : (family CheckpointBlocksValidationResult) .
2089 (eliminate
2090 CheckpointWord64Result
2091 (lambda unrestricted current : (family CheckpointWord64Result) .
2092 (family CheckpointBlocksValidationResult))
2093 (checkpointNaturalWord64
2094 (constructor CheckpointErrorCode CheckpointPayloadLengthOverflow)
2095 (bytes-length payload))
2096 (branch
2097 CheckpointWord64Succeeded
2098 actualLength
2099 .
2100 (nat-eliminate
2101 (lambda unrestricted lengthMatched : Nat .
2102 (family CheckpointBlocksValidationResult))
2103 (constructor
2104 CheckpointBlocksValidationResult
2105 CheckpointBlocksRejected
2106 (checkpointFailure
2107 (constructor
2108 CheckpointErrorCode
2109 CheckpointPayloadLengthMismatch)
2110 zero
2111 (dataBytesWord64LE expectedLength)
2112 (dataBytesWord64LE actualLength))
2113 modelWord64Zero
2114 zero)
2115 (lambda unrestricted lengthPredecessor : Nat .
2116 (lambda unrestricted lengthInduction : (family CheckpointBlocksValidationResult) .
2117 (eliminate
2118 CheckpointBlocksValidationResult
2119 (lambda unrestricted current : (family CheckpointBlocksValidationResult) .
2120 (family CheckpointBlocksValidationResult))
2121 (ih_fields remainingBlocks)
2122 (branch
2123 CheckpointBlocksAccepted
2124 typedTail
2125 tailPayload
2126 tailCount
2127 .
2128 (eliminate
2129 CheckpointWord64Result
2130 (lambda unrestricted current : (family CheckpointWord64Result) .
2131 (family CheckpointBlocksValidationResult))
2132 (checkpointAddChecked
2133 (constructor
2134 CheckpointErrorCode
2135 CheckpointPayloadExtentOverflow)
2136 actualLength
2137 tailPayload)
2138 (branch
2139 CheckpointWord64Succeeded
2140 total
2141 .
2142 (constructor
2143 CheckpointBlocksValidationResult
2144 CheckpointBlocksAccepted
2145 (constructor
2146 CheckpointTypedBlocks
2147 CheckpointTypedBlocksNext
2148 (constructor
2149 CheckpointTypedBlock
2150 CheckpointTypedBlockValue
2151 kind
2152 expectedName
2153 storageOffset
2154 streamOffset
2155 elements
2156 payload)
2157 typedTail)
2158 total
2159 (succ tailCount)))
2160 (branch
2161 CheckpointWord64Failed
2162 code
2163 .
2164 (constructor
2165 CheckpointBlocksValidationResult
2166 CheckpointBlocksRejected
2167 (checkpointSimpleFailure code zero)
2168 tailPayload
2169 tailCount))))
2170 (branch
2171 CheckpointBlocksRejected
2172 failure
2173 payloadBytes
2174 count
2175 .
2176 (eliminate
2177 CheckpointFailure
2178 (lambda unrestricted current : (family CheckpointFailure) .
2179 (family CheckpointBlocksValidationResult))
2180 failure
2181 (branch
2182 CheckpointFailureValue
2183 code
2184 ordinal
2185 expected
2186 actual
2187 .
2188 (constructor
2189 CheckpointBlocksValidationResult
2190 CheckpointBlocksRejected
2191 (checkpointFailure code (succ ordinal) expected actual)
2192 payloadBytes
2193 count)))))))
2194 (modelWord64Equal expectedLength actualLength)))
2195 (branch
2196 CheckpointWord64Failed
2197 code
2198 .
2199 (constructor
2200 CheckpointBlocksValidationResult
2201 CheckpointBlocksRejected
2202 (checkpointSimpleFailure code zero)
2203 modelWord64Zero
2204 zero)))))
2205 (bytes-equal expectedName actualName))))))))))))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.