Data.SHA256Schedule

Linear O(index) message-schedule lookup. The previous definition walked the linked list with a `nat-eliminate` over the FULL index at every node, and its successor step re-invoked the list-recursion hypothesis (`(app induction predecessor)`) at every intermediate fold level. Because the VM evaluates a fold's induction eagerly, one lookup at index k forced a fresh lookup of the tail at 0,1,...,k-1 -- an exponential re-walk that made schedule expansion run in ~O(N^4) (~3.2 billion evals for a single 4-byte hash). A HIGHER-ORDER rewrite (function-valued accumulator) removes the re-invocation but still pays O(k^2) per lookup, because the VM symbolically unrolls the function accumulator into a term of size O(k) at every step. This version is FIRST-ORDER: `sha256ScheduleDrop` folds the SCHEDULE VALUE itself to the suffix at `index` (O(index), shared sub-structures, no term building), then reads that suffix's head word. Result values are byte-for-byte identical to the original (index i still yields W[i]); only the cost changed, so the SHA-256 digest is preserved exactly.

203def sha256ScheduleLookup =
204  (lambda unrestricted schedule : (family SHA256Schedule) .
205    (lambda unrestricted index : Nat .
206      (eliminate
207        SHA256Schedule
208        (lambda unrestricted current : (family SHA256Schedule) .
209          (family SHA256ScheduleLookupResult))
210        (sha256ScheduleDrop index schedule)
211        (branch
212          SHA256ScheduleEnd
213          .
214          (constructor
215            SHA256ScheduleLookupResult
216            SHA256ScheduleLookupFailed
217            (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
218            index))
219        (branch
220          SHA256ScheduleNext
221          word
222          tail
223          nodeInduction
224          .
225          (constructor SHA256ScheduleLookupResult SHA256ScheduleLookupSucceeded word)))))