def conv_lea

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:267

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/nat.bend as N
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/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

267def conv_lea(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hc: {Nat.is_lt(cb(xs, Nat.mul(a, b)), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.conv(xs, ys), cb(xs, Nat.mul(a, b))) == True{} : Bool}:
268  match xs:
269    case Nil{}:
270      {==}
271    case Con{+x, +xt}:
272      +ab = Nat.mul(a, b)
273      +k = cb(xt, ab)
274      +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc)
275      +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc)
276      +hs = scal_lea(one, h1, x, ys, a, b, LM.lea_head(x, xt, a, hx), hy, hab)
277      +hz = L.and_intro(Nat.is_le(0n, k), LM.lea(F.conv(xt, ys), k), N.zero_le(k), conv_lea(one, h1, xt, ys, a, b, LM.lea_tail(x, xt, a, hx), hy, hk))
278      addl_lea(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc)