Data.SHA256Schedule

79def sha256DecodeBlockWordsWithFuel =
80  (lambda unrestricted fuel : Nat .
81    (nat-eliminate
82      (lambda unrestricted current : Nat .
83        (pi unrestricted input : Bytes .
84          (pi unrestricted ordinal : Nat . (family SHA256BlockDecodeResult))))
85      (lambda unrestricted input : Bytes .
86        (lambda unrestricted ordinal : Nat .
87          (nat-eliminate
88            (lambda unrestricted emptyFlag : Nat . (family SHA256BlockDecodeResult))
89            (constructor
90              SHA256BlockDecodeResult
91              SHA256BlockDecodeFailed
92              (constructor SHA256ErrorCode SHA256BlockLengthInvalid)
93              ordinal)
94            (lambda unrestricted predecessor : Nat .
95              (lambda unrestricted induction : (family SHA256BlockDecodeResult) .
96                (constructor
97                  SHA256BlockDecodeResult
98                  SHA256BlockDecodeSucceeded
99                  (constructor SHA256Schedule SHA256ScheduleEnd)
100                  ordinal)))
101            (naturalIsZero (bytes-length input)))))
102      (lambda unrestricted predecessor : Nat .
103        (lambda unrestricted induction : (pi unrestricted input : Bytes . (pi unrestricted ordinal : Nat . (family SHA256BlockDecodeResult))) .
104          (lambda unrestricted input : Bytes .
105            (lambda unrestricted ordinal : Nat .
106              (eliminate
107                SHA256WordReadResult
108                (lambda unrestricted current : (family SHA256WordReadResult) .
109                  (family SHA256BlockDecodeResult))
110                (sha256ReadWord input)
111                (branch
112                  SHA256WordReadSucceeded
113                  word
114                  remaining
115                  .
116                  (eliminate
117                    SHA256BlockDecodeResult
118                    (lambda unrestricted current : (family SHA256BlockDecodeResult) .
119                      (family SHA256BlockDecodeResult))
120                    (induction remaining (succ ordinal))
121                    (branch
122                      SHA256BlockDecodeSucceeded
123                      tailSchedule
124                      finalCount
125                      .
126                      (constructor
127                        SHA256BlockDecodeResult
128                        SHA256BlockDecodeSucceeded
129                        (constructor SHA256Schedule SHA256ScheduleNext word tailSchedule)
130                        finalCount))
131                    (branch
132                      SHA256BlockDecodeFailed
133                      error
134                      failedOrdinal
135                      .
136                      (constructor
137                        SHA256BlockDecodeResult
138                        SHA256BlockDecodeFailed
139                        error
140                        failedOrdinal))))
141                (branch
142                  SHA256WordReadFailed
143                  error
144                  .
145                  (constructor SHA256BlockDecodeResult SHA256BlockDecodeFailed error ordinal)))))))
146      fuel))