Top.public_body_rel: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend as Top Lines 137-147 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&start_line=137&end_line=147 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/spec/crypto/ed25519.bend as SE import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD 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/rel.bend as RL import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as PD import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as BY def public_body_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +D: Nat, +rd: RL.R(pp, PT.cs_d(PT.consts(xs)), D), +rd2: RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, D, D)), +h: List<&2, U32>, +hh: {LM.okb(64n, h, 255n) == True{} : Bool}) -> {E.public_of(PT.consts(xs), xs, h) == SE.public_body(one, 1n+pp, D, h) : List<&2, U32>}: +P = {1n+pp : Nat} +cs = PT.consts(xs) +sk = X.clamp(F.take(32n, h)) +hs = XB.clamp_okb(F.take(32n, h), BY.take_okb(32n, 32n, h, 255n, hh)) +B = PT.base(cs, xs) +SB = SE.base(P, D) +hB = PD.base_rel(one, h1, pp, hP, cs, D, rd, PC.r_sqm1(one, h1, pp, hP, xs), xs) +rm = mul_rel(one, h1, pp, hP, cs, D, rd2, sk, hs, B, SB, hB) +e1 = enc_rel(one, h1, pp, hP, PT.mul(cs, sk, B), SE.mul(one, P, D, FS.value(sk), SB), rm) Equal.trans(List<&2, U32>, PT.encode(PT.mul(cs, sk, B)), SE.encode(one, P, SE.mul(one, P, D, FS.value(sk), SB)), SE.encode(one, P, SE.mul(one, P, D, SE.secret(h), SB)), e1, Equal.cong(Nat, List<&2, U32>, z => SE.encode(one, P, SE.mul(one, P, D, z, SB)), FS.value(sk), SE.secret(h), secret_eq(h))) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=R https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=clamp_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend&name=take_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=r_sqm1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend&name=base_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=enc_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=mul_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=secret_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=fadd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=base https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=public_body https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=secret https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=take https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=clamp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend&name=public_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=base https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=consts https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=cs_d https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=cs_d2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=mul