def conv_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/limbs.bend:92

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/src/crypto/secp256k1/limbs.bend as L
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/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

92def conv_v(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> {ev(L.conv(xs, ys)) == Nat.mul(ev(xs), ev(ys)) : Nat}:
93  match xs:
94    case Nil{}:
95      {==}
96    case +x <> +xt:
97      %Equal.sym(Nat, ev(L.add(L.scal(x, ys), 0n <> L.conv(xt, ys))), Nat.add(ev(L.scal(x, ys)), ev(0n <> L.conv(xt, ys))), add_v(L.scal(x, ys), 0n <> L.conv(xt, ys))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
98      %Equal.sym(Nat, ev(L.scal(x, ys)), Nat.mul(ev(ys), x), scal_v(x, ys)) : {Nat.add(_, ev(0n <> L.conv(xt, ys))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
99      %Equal.sym(Nat, ev(L.conv(xt, ys)), Nat.mul(ev(xt), ev(ys)), conv_v(xt, ys)) : {Nat.add(Nat.mul(ev(ys), x), Nat.add(0n, C.shift(16n, _))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
100      %Equal.sym(Nat, Nat.add(0n, C.shift(16n, Nat.mul(ev(xt), ev(ys)))), C.shift(16n, Nat.mul(ev(xt), ev(ys))), SR.zero_add(C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {Nat.add(Nat.mul(ev(ys), x), _) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
101      %Equal.sym(Nat, Nat.add(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys)))), Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)), NA.add_comm(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
102      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.mul(_, ev(ys)) : Nat}
103      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(xt)), x), ev(ys)), Nat.add(Nat.mul(C.shift(16n, ev(xt)), ev(ys)), Nat.mul(x, ev(ys))), NA.mul_add_right(C.shift(16n, ev(xt)), x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == _ : Nat}
104      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(xt)), ev(ys)), C.shift(16n, Nat.mul(ev(xt), ev(ys))), WW.shift_mul_l(16n, ev(xt), ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(_, Nat.mul(x, ev(ys))) : Nat}
105      %Equal.sym(Nat, Nat.mul(x, ev(ys)), Nat.mul(ev(ys), x), NA.mul_comm(x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), _) : Nat}
106      {==}