def digits_split
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:130
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as Consts
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
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
130def digits_split(+one: Nat, n: Nat, ds: List<&2, Nat>) -> {FS.digits(one, ds) == Nat.add(FS.digits(one, L.take(n, ds)), LV.pos(n, FS.digits(one, L.drop(n, ds)))) : Nat}:
131 match n ds:
132 case 0n Nil{}:
133 {==}
134 case 0n d <> t:
135 {==}
136 case 1n+ +k Nil{}:
137 %Equal.sym(Nat, LV.pos(k, 0n), 0n, LV.pos_zero(k)) : {0n == Nat.add(0n, C.shift(16n, _)) : Nat}
138 %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {0n == Nat.add(0n, _) : Nat}
139 %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {0n == _ : Nat}
140 {==}
141 case 1n+ +k +d <> +t:
142 %Equal.sym(Nat, FS.digits(one, t), Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))), digits_split(one, k, t)) : {Nat.add(Nat.mul(one, d), C.shift(16n, _)) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
143 %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(_, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))))) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
144 %Equal.sym(Nat, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), WW.shift_add(16n, FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))) : {Nat.add(Nat.mul(d, one), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
145 %Equal.sym(Nat, Nat.add(Nat.mul(d, one), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_swap(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {_ == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
146 %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
147 %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(Nat.add(_, C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
148 %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t)))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(_, C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
149 %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_assoc(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == _ : Nat}
150 %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) : Nat}
151 {==}