Top.sign_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 173-196 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=173&end_line=196 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/spec/crypto/sha512.bend as SHA import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H 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/scalar.bend as ESC 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/scalar3.bend as S3 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 sign_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}, +msg: List<&2, U32>) -> {E.sign_with(PT.consts(xs), xs, h, msg) == SE.sign_body(one, 1n+pp, D, h, msg) : List<&2, U32>}: +P = {1n+pp : Nat} +el = SE.ell(one) +cs = PT.consts(xs) +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) +A = E.public_of(cs, xs, h) +SA = SE.public_of(one, P, D, h) +RH = E.cat(F.drop(32n, h), msg) +SRH = SE.cat(SE.rest(32n, h), msg) +r = ESC.reduce(H.sha512(RH)) +Rs = Nat.mod(FS.value(SHA.sha512_bytes(SRH)), el) +eR = rh_eq(one, h1, RH, SRH, prefix_eq(h, msg)) +okr = S3.reduce_okb(one, h1, H.sha512(RH), BY.sha_lea(RH)) +RB = PT.encode(PT.mul(cs, r, B)) +SRB = SE.encode(one, P, SE.mul(one, P, D, Rs, SB)) +eRB = rb_eq(one, h1, pp, hP, cs, D, rd2, B, SB, hB, r, okr, Rs, eR) +k = E.hram(RB, A, msg) +Ks = SE.hram(one, SRB, SA, msg) +eK = hk_val(one, h1, RB, SRB, eRB, A, SA, public_rel(one, h1, pp, hP, xs, D, rd, rd2, h, hh), msg) +sk = X.clamp(F.take(32n, h)) +hsk = XB.clamp_okb(F.take(32n, h), BY.take_okb(32n, 32n, h, 255n, hh)) sig_eq(one, h1, RB, SRB, eRB, k, hk_okb(one, h1, RB, A, msg), Ks, eK, r, okr, red_lt(one, h1, H.sha512(RH), BY.sha_lea(RH)), Rs, eR, sk, hsk, SE.secret(h), secret_eq(h)) Uses (52): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=Nat.mod 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=sha_lea 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/scalar3.bend&name=reduce_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=hk_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=hk_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=prefix_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=public_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=rb_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=red_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend&name=rh_eq 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/crypto/ed25519/top.bend&name=sig_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=cat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=ell 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=hram 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_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=rest 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/spec/crypto/ed25519.bend&name=sign_body https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=sha512_bytes https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=drop 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=cat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend&name=hram 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/ed25519.bend&name=sign_with 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 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend&name=reduce https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=sha512