def carry_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/limbs.bend:195
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as Limbs
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/math/typed/width.bend as WW
195
196def carry_v(n: Nat, xs: List<&2, Nat>, +u: Nat) -> {ev(L.carry(n, xs, u)) == Nat.add(u, ev(xs)) : Nat}:
197 match n xs:
198 case 0n Nil{}:
199 %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(u, _) == Nat.add(u, 0n) : Nat}
200 %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {_ == Nat.add(u, 0n) : Nat}
201 %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {u == _ : Nat}
202 {==}
203 case 0n +x <> +t:
204 %Equal.sym(Nat, L.horner(x <> t), ev(x <> t), horner_v(x <> t)) : {Nat.add(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
205 %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(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
206 %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(_, C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
207 %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
208 %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), 0n), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_zero(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
209 %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)), Nat.add(u, x)) == Nat.add(u, _) : Nat}
210 %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat}
211 {==}
212 case 1n+ +k Nil{}:
213 %Equal.sym(Nat, ev(L.carry(k, [], L.hi16(Nat.add(u, 0n)))), Nat.add(L.hi16(Nat.add(u, 0n)), ev([])), carry_v(k, [], L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat}
214 %Equal.sym(Nat, Nat.add(L.hi16(Nat.add(u, 0n)), 0n), L.hi16(Nat.add(u, 0n)), NA.add_zero(L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat}
215 %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, L.hi16(Nat.add(u, 0n)))), Nat.add(u, 0n), lohi(Nat.add(u, 0n))) : {_ == Nat.add(u, 0n) : Nat}
216 {==}
217 case 1n+ +k +x <> +t:
218 %Equal.sym(Nat, ev(L.carry(k, t, L.hi16(Nat.add(u, x)))), Nat.add(L.hi16(Nat.add(u, x)), ev(t)), carry_v(k, t, L.hi16(Nat.add(u, x)))) : {Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, _)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
219 %Equal.sym(Nat, C.shift(16n, Nat.add(L.hi16(Nat.add(u, x)), ev(t))), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))), WW.shift_add(16n, L.hi16(Nat.add(u, x)), ev(t))) : {Nat.add(L.lo16(Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
220 %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Equal.sym(Nat, Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), NA.add_assoc(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
221 %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), Nat.add(u, x), lohi(Nat.add(u, x))) : {Nat.add(_, C.shift(16n, ev(t))) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
222 %Equal.sym(Nat, Nat.add(Nat.add(u, x), C.shift(16n, ev(t))), Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))), NA.add_assoc(u, x, C.shift(16n, ev(t)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
223 %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(u, _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
224 %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
225 %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)), Nat.add(u, x)) == Nat.add(u, _) : Nat}
226 %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat}
227 {==}