Poly.conv_val: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly Lines 280-301 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&start_line=280&end_line=301 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/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/lib/arith.bend as AR 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/num.bend as M import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM def conv_val(+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}) -> {FS.value(F.conv(xs, ys)) == Nat.mul(FS.value(xs), FS.value(ys)) : Nat}: match xs: case Nil{}: {==} case Con{+x, +xt}: +ab = Nat.mul(a, b) +k = cb(xt, ab) +Y = FS.value(ys) +X = FS.value(xt) +hab = N.le_lt_trans(ab, Nat.add(ab, k), WD.sc(32n, one), N.le_add_right(ab, k), hc) +hk = N.le_lt_trans(k, Nat.add(ab, k), WD.sc(32n, one), le_add_l(ab, k), hc) +hxh = LM.lea_head(x, xt, a, hx) +hxt = LM.lea_tail(x, xt, a, hx) +hs = scal_lea(one, h1, x, ys, a, b, hxh, hy, hab) +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, hxt, hy, hk)) +e1 = addl_val(one, h1, F.scal(x, ys), Con{0, F.conv(xt, ys)}, ab, k, hs, hz, hc) +e2 = M.cong_add(FS.value(F.scal(x, ys)), Nat.mul(v(x), Y), FS.value(Con{0, F.conv(xt, ys)}), C.shift(8n, Nat.mul(X, Y)), scal_val(one, h1, x, ys, a, b, hxh, hy, hab), M.cong_sc(8n, FS.value(F.conv(xt, ys)), Nat.mul(X, Y), conv_val(one, h1, xt, ys, a, b, hxt, hy, hk))) +e3 = M.cong_r(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y)), Nat.mul(C.shift(8n, X), Y), AR.sc_mul(8n, X, Y)) +e4 = Equal.sym(Nat, Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), NA.mul_add_right(v(x), C.shift(8n, X), Y)) Equal.trans(Nat, FS.value(F.conv(Con{x, xt}, ys)), Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e1, Equal.trans(Nat, Nat.add(FS.value(F.scal(x, ys)), FS.value(Con{0, F.conv(xt, ys)})), Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e2, Equal.trans(Nat, Nat.add(Nat.mul(v(x), Y), C.shift(8n, Nat.mul(X, Y))), Nat.add(Nat.mul(v(x), Y), Nat.mul(C.shift(8n, X), Y)), Nat.mul(Nat.add(v(x), C.shift(8n, X)), Y), e3, e4))) Uses (34): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul 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=lea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_head https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_tail https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=addl_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=cb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=conv_lea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=le_add_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=scal_lea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=scal_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=sc_mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_intro https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=zero_le 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=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=conv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=scal