First-order prefix take.
The previous definition folded a FUNCTION accumulator (`pi input . Bytes`) and,
worse, used `bytes-eliminate` inside the step. The VM's bytes recursor EAGERLY
evaluates the tail's recursive result before the branch (which ignores it)
runs, so composing it under the fuel fold re-walked every suffix at every
level -- an exponential that made even `take 64` of a 64-byte LITERAL cost
minutes and gigabytes, which then fed a non-literal block into decode/expand
and blew those up in turn. This version folds a FIRST-ORDER value accumulator
(taken prefix + remaining bytes) built only from the O(1) native primitives
bytes-head / bytes-tail / bytes-cons / bytes-append, so a take over a literal
stays a literal and costs O(fuel^2) bounded work. For the 64-aligned blocks the
digest driver slices, the bytes produced are identical, so the digest is
preserved exactly.
657def sha256DigestTakeWithFuel =
658 (lambda unrestricted fuel : Nat .
659 (lambda unrestricted input : Bytes .
660 (eliminate
661 SHA256BytesSplit
662 (lambda unrestricted current : (family SHA256BytesSplit) . Bytes)
663 (nat-eliminate
664 (lambda unrestricted current : Nat . (family SHA256BytesSplit))
665 (constructor SHA256BytesSplit SHA256BytesSplitValue b"" input)
666 (lambda unrestricted predecessor : Nat .
667 (lambda unrestricted induction : (family SHA256BytesSplit) .
668 (eliminate
669 SHA256BytesSplit
670 (lambda unrestricted current : (family SHA256BytesSplit) .
671 (family SHA256BytesSplit))
672 induction
673 (branch
674 SHA256BytesSplitValue
675 taken
676 rest
677 .
678 (constructor
679 SHA256BytesSplit
680 SHA256BytesSplitValue
681 (bytes-append taken (bytes-cons (bytes-head rest) b""))
682 (bytes-tail rest))))))
683 fuel)
684 (branch SHA256BytesSplitValue taken rest . taken))))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.