def valo_u
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/adc.bend:105
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as Adc
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
105def valo_u(+one: Nat, +xs: List<&2, U32>) -> {K.valo(one, xs) == FS.uvalue(one, xs) : Nat}:
106 match xs:
107 case Nil{}:
108 {==}
109 case Con{+x, +xt}:
110 M.cong_r(Nat.mul(one, v(x)), C.shift(8n, K.valo(one, xt)), C.shift(8n, FS.uvalue(one, xt)), M.cong_sc(8n, K.valo(one, xt), FS.uvalue(one, xt), valo_u(one, xt)))