def scal_v

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

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

76def scal_v(+a: Nat, ys: List<&2, Nat>) -> {ev(L.scal(a, ys)) == Nat.mul(ev(ys), a) : Nat}:
77  match ys:
78    case Nil{}:
79      {==}
80    case +y <> +yt:
81      %Equal.sym(Nat, ev(L.scal(a, yt)), Nat.mul(ev(yt), a), scal_v(a, yt)) : {Nat.add(Nat.mul(y, a), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
82      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(_, C.shift(16n, Nat.mul(ev(yt), a))) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
83      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(Nat.mul(a, y), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
84      %Equal.sym(Nat, Nat.add(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt)))), Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)), NA.add_comm(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt))))) : {_ == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
85      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.mul(_, a) : Nat}
86      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(yt)), y), a), Nat.add(Nat.mul(C.shift(16n, ev(yt)), a), Nat.mul(y, a)), NA.mul_add_right(C.shift(16n, ev(yt)), y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == _ : Nat}
87      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(yt)), a), C.shift(16n, Nat.mul(ev(yt), a)), WW.shift_mul_l(16n, ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(_, Nat.mul(y, a)) : Nat}
88      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, _), Nat.mul(y, a)) : Nat}
89      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), _) : Nat}
90      {==}