127def sha256ValidateContext =
128 (lambda unrestricted context : (family SHA256Context) .
129 (eliminate
130 SHA256Context
131 (lambda unrestricted current : (family SHA256Context) .
132 (family SHA256ContextValidationResult))
133 context
134 (branch
135 SHA256ContextValue
136 state
137 totalBytes
138 pending
139 .
140 (app
141 (lambda unrestricted pendingBytes : Nat .
142 (app
143 (lambda unrestricted totalRemainder : Nat .
144 (app
145 (lambda unrestricted withinLimit : Nat .
146 (app
147 (lambda unrestricted telemetry : (family SHA256ContextValidationTelemetry) .
148 (nat-eliminate
149 (lambda unrestricted pendingValid : Nat .
150 (family SHA256ContextValidationResult))
151 (constructor
152 SHA256ContextValidationResult
153 SHA256ContextValidationFailed
154 (constructor SHA256ErrorCode SHA256PendingBlockTooLarge)
155 telemetry)
156 (lambda unrestricted pendingPredecessor : Nat .
157 (lambda unrestricted pendingInduction : (family SHA256ContextValidationResult) .
158 (nat-eliminate
159 (lambda unrestricted lengthValid : Nat .
160 (family SHA256ContextValidationResult))
161 (constructor
162 SHA256ContextValidationResult
163 SHA256ContextValidationFailed
164 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
165 telemetry)
166 (lambda unrestricted lengthPredecessor : Nat .
167 (lambda unrestricted lengthInduction : (family SHA256ContextValidationResult) .
168 (nat-eliminate
169 (lambda unrestricted congruent : Nat .
170 (family SHA256ContextValidationResult))
171 (constructor
172 SHA256ContextValidationResult
173 SHA256ContextValidationFailed
174 (constructor SHA256ErrorCode SHA256ContextLengthMismatch)
175 telemetry)
176 (lambda unrestricted congruentPredecessor : Nat .
177 (lambda unrestricted congruentInduction : (family SHA256ContextValidationResult) .
178 (constructor
179 SHA256ContextValidationResult
180 SHA256ContextValidated
181 context
182 telemetry)))
183 (naturalEqual pendingBytes totalRemainder))))
184 withinLimit)))
185 (naturalLess pendingBytes sha256NaturalSixtyFour)))
186 (constructor
187 SHA256ContextValidationTelemetry
188 SHA256ContextValidationTelemetryValue
189 totalBytes
190 pendingBytes
191 totalRemainder
192 withinLimit)))
193 (sha256Word64WithinInputLimit totalBytes)))
194 (sha256Word64ModuloBlockBytes totalBytes)))
195 (bytes-length pending)))))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.