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