169def sha256ExpandScheduleStep =
170 (lambda unrestricted state : (family SHA256ScheduleExpansionState) .
171 (eliminate
172 SHA256ScheduleExpansionState
173 (lambda unrestricted current : (family SHA256ScheduleExpansionState) .
174 (family SHA256ScheduleExpansionStepResult))
175 state
176 (branch
177 SHA256ScheduleExpansionStateValue
178 schedule
179 nextIndex
180 generated
181 lookups
182 sigmas
183 rotates
184 shifts
185 adds
186 .
187 (eliminate
188 SHA256ScheduleDependenciesResult
189 (lambda unrestricted current : (family SHA256ScheduleDependenciesResult) .
190 (family SHA256ScheduleExpansionStepResult))
191 (sha256LookupScheduleDependencies schedule nextIndex)
192 (branch
193 SHA256ScheduleDependenciesSucceeded
194 wordMinus2
195 wordMinus7
196 wordMinus15
197 wordMinus16
198 .
199 (app
200 (lambda unrestricted generatedWord : (family ModelWord32) .
201 (constructor
202 SHA256ScheduleExpansionStepResult
203 SHA256ScheduleExpansionStepSucceeded
204 (constructor
205 SHA256ScheduleExpansionState
206 SHA256ScheduleExpansionStateValue
207 (sha256ScheduleAppend schedule generatedWord)
208 (succ nextIndex)
209 (succ generated)
210 (naturalAdd lookups sha256NaturalFour)
211 (naturalAdd sigmas sha256NaturalTwo)
212 (naturalAdd rotates sha256NaturalFour)
213 (naturalAdd shifts sha256NaturalTwo)
214 (naturalAdd adds (byte-to-nat (byte 3))))))
215 (modelWord32AddFour
216 (sha256SmallSigma1 wordMinus2)
217 wordMinus7
218 (sha256SmallSigma0 wordMinus15)
219 wordMinus16)))
220 (branch
221 SHA256ScheduleDependenciesFailed
222 error
223 failedIndex
224 .
225 (constructor
226 SHA256ScheduleExpansionStepResult
227 SHA256ScheduleExpansionStepFailed
228 error
229 failedIndex))))))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.