def ma_eq

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/curve25519/x25519.bend as SX
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/ed25519/scalar.bend as ESC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
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/cong.bend as G
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

100# S = (r + k s) mod L, as 32 bytes: s reduced first (the implementation's
101# reduce(secret)), the same residue
102def ma_eq(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +r: List<&2, U32>, +sk: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}, +hr: {LM.okb(32n, r, 255n) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+S3.mmL(one)) == True{} : Bool}, +hsk: {LM.okb(32n, sk, 255n) == True{} : Bool}, +Rs: Nat, +Ks: Nat, +Ss: Nat, +eR: {FS.value(r) == Rs : Nat}, +eK: {FS.value(k) == Ks : Nat}, +eS: {FS.value(sk) == Ss : Nat}) -> {ESC.mul_add(k, ESC.reduce(sk), r) == SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), SE.ell(one))) : List<&2, U32>}:
103  +mm = S3.mmL(one)
104  +M = {1n+S3.mmL(one) : Nat}
105  +el = SE.ell(one)
106  +s = ESC.reduce(sk)
107  +hl = LM.okb_lea(32n, sk, 255n, hsk)
108  +lk = LM.okb_lea(32n, k, 255n, hk)
109  +os = S3.reduce_okb(one, h1, sk, hl)
110  +ls = red_lt(one, h1, sk, hl)
111  +MA = ESC.mul_add(k, s, r)
112  +Vr = FS.value(r)
113  +Vk = FS.value(k)
114  +Vs = FS.value(sk)
115  +T0 = FS.value(MA)
116  +T1 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, FS.value(s))), M)
117  +T2 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, Nat.mod(Vs, M))), M)
118  +T3 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, Vs)), M)
119  +T4 = Nat.mod(Nat.add(Rs, Nat.mul(Vk, Vs)), M)
120  +T5 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Vs)), M)
121  +T6 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), M)
122  +T7 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), el)
123  +e0 = S3.mul_add_m(one, h1, k, s, r, lk, os, hr, ls, lr)
124  +e1 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Vr, Nat.mul(Vk, z)), M), FS.value(s), Nat.mod(Vs, M), S3.reduce_m(one, h1, sk, hl))
125  +e2 = G.c_add(mm, Vr, Vr, Nat.mul(Vk, Nat.mod(Vs, M)), Nat.mul(Vk, Vs), G.c_refl(mm, Vr), G.c_mul(mm, Vk, Vk, Nat.mod(Vs, M), Vs, G.c_refl(mm, Vk), G.c_mod(mm, Vs)))
126  +e3 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, Nat.mul(Vk, Vs)), M), Vr, Rs, eR)
127  +e4 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(z, Vs)), M), Vk, Ks, eK)
128  +e5 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(Ks, z)), M), Vs, Ss, eS)
129  +e6 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), z), M, el, S3.ell_eq(one, h1))
130  +ev = Equal.trans(Nat, T0, T1, T7, e0, Equal.trans(Nat, T1, T2, T7, e1, Equal.trans(Nat, T2, T3, T7, e2, Equal.trans(Nat, T3, T4, T7, e3, Equal.trans(Nat, T4, T5, T7, e4, Equal.trans(Nat, T5, T6, T7, e5, e6))))))
131  +eb = Equal.sym(List<&2, U32>, SX.le_bytes(32n, T0), MA, XB.bytes_le(32n, MA, S3.mul_add_lt(one, h1, k, s, r, lk, os, hr, ls, lr)))
132  +e8 = Equal.trans(List<&2, U32>, MA, SX.le_bytes(32n, T0), SX.le_bytes(32n, T7), eb, Equal.cong(Nat, List<&2, U32>, z => SX.le_bytes(32n, z), T0, T7, ev))
133  L.subst(Nat, z => {MA == SX.le_bytes(z, T7) : List<&2, U32>}, 32n, C.shift(5n, one), Equal.cong(Nat, Nat, z => C.shift(5n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)), e8)