proofs/crypto/secp256k1/ppub.bend source
proofs/crypto/secp256k1/ppub.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/ppub.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/ecdsa.bend as ESimport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/point.bend as Pimport ../../../src/crypto/secp256k1/ecdsa.bend as Eimport ./bytes.bend as BYimport ./point.bend as PTimport ./pmul.bend as PMimport ./paff.bend as PAimport ./penc.bend as PEimport ./blist.bend as BLimport ./pscal.bend as SQ# Scalars from bytes and public keys of src/crypto/secp256k1/ecdsa.bend# against spec/crypto/secp256k1/ecdsa.bend.# ---- scalars ----def pk_v(+one: Nat, +h1: {one == 1n : Nat}, c: Bool, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {E.pk_of(c, q) == ES.pk_of(one, c, PT.pv(one, q)) : List<&2, U32>}: match c: case True{}: PE.encode_compressed_v(one, h1, q, hq) case False{}: PE.encode_uncompressed_v(one, h1, q, hq)# [d] Gdef pubpt_v(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.limbs16(one, 16n, d) == True{} : Bool}) -> {PT.pv(one, E.public_point(d)) == CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)) : CV.SPoint}: %Equal.sym(CV.SPoint, PT.pv(one, P.mul(d, P.g())), CV.pmul(FS.prime(one), FS.value(one, d), PT.pv(one, P.g())), PM.mul_v(one, h1, d, P.g(), hd, PA.g_r(one, h1))) : {_ == CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)) : CV.SPoint} %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {CV.pmul(FS.prime(one), FS.value(one, d), _) == CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)) : CV.SPoint} {==}def pubpt_r(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.limbs16(one, 16n, d) == True{} : Bool}) -> {PT.pred(one, E.public_point(d)) == True{} : Bool}: PM.mul_r(one, h1, d, P.g(), hd, PA.g_r(one, h1))def pub_ok(+one: Nat, +h1: {one == 1n : Nat}, c: Bool, +d: List<&2, Nat>, +hd: {FS.limbs16(one, 16n, d) == True{} : Bool}, b: Bool) -> {E.public_key_d(c, E.secret_if(d, b)) == ES.public_d(one, c, FS.value(one, d), b) : Maybe<&2, List<&2, U32>>}: match b: case True{}: %Equal.sym(List<&2, U32>, E.pk_of(c, E.public_point(d)), ES.pk_of(one, c, PT.pv(one, E.public_point(d))), pk_v(one, h1, c, E.public_point(d), pubpt_r(one, h1, d, hd))) : {Some{_} == Some{ES.pk_of(one, c, CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)))} : Maybe<&2, List<&2, U32>>} %Equal.sym(CV.SPoint, PT.pv(one, E.public_point(d)), CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)), pubpt_v(one, h1, d, hd)) : {Some{ES.pk_of(one, c, _)} == Some{ES.pk_of(one, c, CV.pmul(FS.prime(one), FS.value(one, d), CV.g(one)))} : Maybe<&2, List<&2, U32>>} {==} case False{}: {==}def pub_len(+one: Nat, +h1: {one == 1n : Nat}, c: Bool, +sk: List<&2, U32>, a: Bool, +ha: {B.has_len(32n, sk) == a : Bool}) -> {E.public_key_d(c, E.secret_if(B.of_be(sk), Bool.and(a, E.scalar_ok(B.of_be(sk))))) == ES.public_d(one, c, CV.os2ip(sk), Bool.and(a, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}: match a: case True{}: +hd = BY.of_be_limbs(one, h1, sk, ha) %Equal.sym(Bool, E.scalar_ok(B.of_be(sk)), ES.scalar_ok(one, FS.value(one, B.of_be(sk))), SQ.scalar_ok_v(one, h1, B.of_be(sk))) : {E.public_key_d(c, E.secret_if(B.of_be(sk), Bool.and(a, _))) == ES.public_d(one, c, CV.os2ip(sk), Bool.and(a, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {E.public_key_d(c, E.secret_if(B.of_be(sk), Bool.and(a, ES.scalar_ok(one, FS.value(one, B.of_be(sk)))))) == ES.public_d(one, c, _, Bool.and(a, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>} %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {E.public_key_d(c, E.secret_if(B.of_be(sk), Bool.and(a, ES.scalar_ok(one, FS.value(one, B.of_be(sk)))))) == ES.public_d(one, c, FS.value(one, B.of_be(sk)), Bool.and(a, ES.scalar_ok(one, _))) : Maybe<&2, List<&2, U32>>} pub_ok(one, h1, c, B.of_be(sk), hd, ES.scalar_ok(one, FS.value(one, B.of_be(sk)))) case False{}: {==}# the SEC 1 public key of a secret keydef public_key_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, c: Bool) -> {E.public_key(sk, c) == ES.public_key(one, sk, c) : Maybe<&2, List<&2, U32>>}: %Equal.sym(Bool, B.has_len(32n, sk), CV.length_is(32n, sk), BL.hl_is(32n, sk)) : {E.public_key_d(c, E.secret_if(B.of_be(sk), Bool.and(_, E.scalar_ok(B.of_be(sk))))) == ES.public_d(one, c, CV.os2ip(sk), Bool.and(CV.length_is(32n, sk), ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>} pub_len(one, h1, c, sk, CV.length_is(32n, sk), BL.hl_is(32n, sk))