def r_valo

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:76

import Base
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/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL

76# a constant given through its valo, the list kept a variable
77def r_valo(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +ks: List<&2, U32>, +D: Nat, +hv: {K.valo(one, ks) == D : Nat}, +ho: {LM.okb(32n, ks, 255n) == True{} : Bool}) -> RL.R(pp, ks, D):
78  (ho, G.c_eq(pp, FS.value(ks), D, Equal.trans(Nat, FS.value(ks), K.valo(one, ks), D, Equal.sym(Nat, K.valo(one, ks), FS.value(ks), K.valo_value(one, h1, ks)), hv)))