def add_v

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

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

54def add_v(xs: List<&2, Nat>, ys: List<&2, Nat>) -> {ev(L.add(xs, ys)) == Nat.add(ev(xs), ev(ys)) : Nat}:
55  match xs ys:
56    case Nil{} Nil{}:
57      {==}
58    case Nil{} y <> yt:
59      {==}
60    case +x <> +xt Nil{}:
61      Equal.sym(Nat, Nat.add(ev(x <> xt), 0n), ev(x <> xt), NA.add_zero(ev(x <> xt)))
62    case +x <> +xt +y <> +yt:
63      %Equal.sym(Nat, ev(L.add(xt, yt)), Nat.add(ev(xt), ev(yt)), add_v(xt, yt)) : {Nat.add(Nat.add(x, y), C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
64      %Equal.sym(Nat, C.shift(16n, Nat.add(ev(xt), ev(yt))), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))), WW.shift_add(16n, ev(xt), ev(yt))) : {Nat.add(Nat.add(x, y), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
65      %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(x, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))), NA.add_assoc(x, y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
66      %Equal.sym(Nat, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(C.shift(16n, ev(xt)), Nat.add(y, C.shift(16n, ev(yt)))), NA.add_swap(y, C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
67      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(x, Nat.add(C.shift(16n, ev(xt)), _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
68      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_swap(x, C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
69      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
70      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(_, Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
71      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(Nat.add(C.shift(16n, ev(xt)), x), _) : Nat}
72      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(xt)), x), Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_assoc(C.shift(16n, ev(xt)), x, Nat.add(C.shift(16n, ev(yt)), y))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == _ : Nat}
73      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(C.shift(16n, ev(xt)), _) : Nat}
74      {==}