def sub_go

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldops.bend:136

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/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

136# F.sub looks at a first; a reduced a has 16 limbs
137def sub_go(+one: Nat, +h1: {one == 1n : Nat}, a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {F.sub(a, b) == F.reduce(L.add(a, L.neg_raw(F.c(), b))) : List<&2, Nat>}:
138  match a:
139    case Nil{}:
140      Empty.absurd({F.sub([], b) == F.reduce(L.add([], L.neg_raw(F.c(), b))) : List<&2, Nat>}, Lg.false_true(Lg.and_left(FS.limbs16(one, 16n, []), Nat.is_lt(FS.value(one, []), FS.prime(one)), ha)))
141    case x <> t:
142      {==}