def horner_v

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

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/crypto/secp256k1/semiring.bend as SR

183def horner_v(xs: List<&2, Nat>) -> {L.horner(xs) == ev(xs) : Nat}:
184  match xs:
185    case Nil{}:
186      {==}
187    case +x <> +t:
188      %Equal.sym(Nat, L.horner(t), ev(t), horner_v(t)) : {Nat.add(Nat.mul(Nat.mul(_, 256n), 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
189      %Equal.sym(Nat, Nat.mul(ev(t), 256n), C.shift(8n, ev(t)), m256(ev(t))) : {Nat.add(Nat.mul(_, 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
190      %Equal.sym(Nat, Nat.mul(C.shift(8n, ev(t)), 256n), C.shift(8n, C.shift(8n, ev(t))), m256(C.shift(8n, ev(t)))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
191      %Equal.sym(Nat, C.shift(8n, C.shift(8n, ev(t))), C.shift(16n, ev(t)), SR.shift_shift(8n, 8n, ev(t))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
192      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), x) == _ : Nat}
193      {==}