def hv_p

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pdec.bend:35

import Base
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/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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/freeze.bend as FZ
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M3

35# y >= p exactly when the carry of y + 2^256 - p is not 0
36def hv_p(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(K.valo(one, F.comp_p()), 1n+pp) == SC.T(one) : Nat}:
37  +P = {1n+pp : Nat}
38  +e1 = M3.cong_l(K.valo(one, F.comp_p()), Nat.add(P, 38n), P, FZ.comp_p_val(one, h1, pp, hP))
39  +e2 = Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(P, Nat.add(38n, P)), Nat.add(Nat.add(P, P), 38n), NA.add_assoc(P, 38n, P), Equal.trans(Nat, Nat.add(P, Nat.add(38n, P)), Nat.add(P, Nat.add(P, 38n)), Nat.add(Nat.add(P, P), 38n), M3.cong_r(P, Nat.add(38n, P), Nat.add(P, 38n), NA.add_comm(38n, P)), Equal.sym(Nat, Nat.add(Nat.add(P, P), 38n), Nat.add(P, Nat.add(P, 38n)), NA.add_assoc(P, P, 38n))))
40  Equal.trans(Nat, Nat.add(K.valo(one, F.comp_p()), P), Nat.add(Nat.add(P, 38n), P), SC.T(one), e1, Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(Nat.add(P, P), 38n), SC.T(one), e2, Equal.sym(Nat, SC.T(one), Nat.add(Nat.add(P, P), 38n), FZ.t_val(one, h1, pp, hP))))