The only public Bytes -> SHA256Digest boundary. The equality witness is
erased, but the ordinary kernel still checks that construction is possible
only when the byte sequence is exactly 32 bytes long.
122def sha256DigestFromBytes : (pi unrestricted input : Bytes . (family SHA256Result)) =
123 (lambda unrestricted input : Bytes .
124 (app
125 (eliminate
126 SHA256DigestLengthValidity
127 (lambda unrestricted decision : (family SHA256DigestLengthValidity) .
128 (pi erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) decision) .
129 (family SHA256Result)))
130 (nat-eliminate
131 (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity))
132 (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)
133 (lambda unrestricted predecessor : Nat .
134 (lambda unrestricted induction : (family SHA256DigestLengthValidity) .
135 (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)))
136 (naturalEqual (bytes-length input) (byte-to-nat (byte 32))))
137 (branch
138 SHA256DigestLengthValid
139 .
140 (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)) .
141 (constructor
142 SHA256Result
143 SHA256Succeeded
144 (constructor SHA256Digest SHA256DigestValue input witness))))
145 (branch
146 SHA256DigestLengthInvalid
147 .
148 (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)) .
149 (constructor
150 SHA256Result
151 SHA256Failed
152 (constructor SHA256ErrorCode SHA256DigestLengthInvalid)))))
153 (refl
154 (family SHA256DigestLengthValidity)
155 (nat-eliminate
156 (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity))
157 (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)
158 (lambda unrestricted predecessor : Nat .
159 (lambda unrestricted induction : (family SHA256DigestLengthValidity) .
160 (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)))
161 (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))))))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.