def pow_is

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/scalarpow.bend:71

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

71# S.pow looks at x first
72def pow_is(+one: Nat, x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>) -> {S.pow(x, bs, acc) == S.pow_go(x, bs, acc) : List<&2, Nat>}:
73  match x:
74    case Nil{}:
75      Empty.absurd({S.pow([], bs, acc) == S.pow_go([], bs, acc) : List<&2, Nat>}, Lg.false_true(Lg.and_left(FS.limbs16(one, 16n, []), Nat.is_lt(FS.value(one, []), FS.order(one)), hx)))
76    case y <> t:
77      {==}