def conv_len_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:303

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F

303def conv_len_ge(+n: Nat, +x: U32, +xt: List<&2, U32>, +ys: List<&2, U32>, +e: {len_ge(n, ys) == True{} : Bool}) -> {len_ge(n, F.conv(Con{x, xt}, ys)) == True{} : Bool}:
304  addl_len_ge(n, F.scal(x, ys), Con{0, F.conv(xt, ys)}, scal_len_ge(n, x, ys, e))