def sign_body_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/top.bend:173

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

173def 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>}:
174  +P = {1n+pp : Nat}
175  +el = SE.ell(one)
176  +cs = PT.consts(xs)
177  +B = PT.base(cs, xs)
178  +SB = SE.base(P, D)
179  +hB = PD.base_rel(one, h1, pp, hP, cs, D, rd, PC.r_sqm1(one, h1, pp, hP, xs), xs)
180  +A = E.public_of(cs, xs, h)
181  +SA = SE.public_of(one, P, D, h)
182  +RH = E.cat(F.drop(32n, h), msg)
183  +SRH = SE.cat(SE.rest(32n, h), msg)
184  +r = ESC.reduce(H.sha512(RH))
185  +Rs = Nat.mod(FS.value(SHA.sha512_bytes(SRH)), el)
186  +eR = rh_eq(one, h1, RH, SRH, prefix_eq(h, msg))
187  +okr = S3.reduce_okb(one, h1, H.sha512(RH), BY.sha_lea(RH))
188  +RB = PT.encode(PT.mul(cs, r, B))
189  +SRB = SE.encode(one, P, SE.mul(one, P, D, Rs, SB))
190  +eRB = rb_eq(one, h1, pp, hP, cs, D, rd2, B, SB, hB, r, okr, Rs, eR)
191  +k = E.hram(RB, A, msg)
192  +Ks = SE.hram(one, SRB, SA, msg)
193  +eK = hk_val(one, h1, RB, SRB, eRB, A, SA, public_rel(one, h1, pp, hP, xs, D, rd, rd2, h, hh), msg)
194  +sk = X.clamp(F.take(32n, h))
195  +hsk = XB.clamp_okb(F.take(32n, h), BY.take_okb(32n, 32n, h, 255n, hh))
196  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))