def pdbl_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:226
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as Point
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/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
226def pdbl_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {pred(one, a) == True{} : Bool}) -> {pv(one, P.dbl(a)) == CV.pdbl(FS.prime(one), pv(one, a)) : CV.SPoint}:
227 match a:
228 case P.Point{+x, +y, +z}:
229 +hr = regs4(one, h1, x, y, z, ha)
230 %Equal.sym(Nat, FS.value(one, P.nth(21n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 21n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{_, FS.value(one, P.nth(18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
231 %Equal.sym(Nat, FS.value(one, P.nth(18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), _, FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
232 %Equal.sym(Nat, FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 13n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), _} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
233 %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, _), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
234 %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, _), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
235 %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, _)} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
236 %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
237 %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
238 %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
239 %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), _)), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
240 %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), _)), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
241 %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), _))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
242 %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
243 %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
244 %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
245 {==}