def digest_okb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/bytes.bend:132

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

132def digest_okb(+s: T512.State) -> {LM.okb(64n, C512.digest_bytes(s), 255n) == True{} : Bool}:
133  match s:
134    case T512.H{+a, +b, +c, +d, +e, +f, +g, +h}:
135      +th = C512.lane_octets(h, Nil{})
136      +tg = C512.lane_octets(g, th)
137      +tf = C512.lane_octets(f, tg)
138      +te = C512.lane_octets(e, tf)
139      +td = C512.lane_octets(d, te)
140      +tc = C512.lane_octets(c, td)
141      +tb = C512.lane_octets(b, tc)
142      lane_okb(56n, a, tb, lane_okb(48n, b, tc, lane_okb(40n, c, td, lane_okb(32n, d, te, lane_okb(24n, e, tf, lane_okb(16n, f, tg, lane_okb(8n, g, th, lane_okb(0n, h, Nil{}, {==}))))))))