def ev_value

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

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/secp256k1/field.bend as FS

43def ev_value(+one: Nat, +h1: {one == 1n : Nat}, xs: List<&2, Nat>) -> {FS.value(one, xs) == ev(xs) : Nat}:
44  match xs:
45    case Nil{}:
46      {==}
47    case +x <> +t:
48      %Equal.sym(Nat, Nat.mul(one, x), x, mul_one_l(one, h1, x)) : {Nat.add(_, C.shift(16n, FS.digits(one, t))) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
49      %Equal.sym(Nat, FS.digits(one, t), ev(t), ev_value(one, h1, t)) : {Nat.add(x, C.shift(16n, _)) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
50      {==}