~/jendhub

proofs/crypto/secp256k1/ppub.bend

bend-collections-laws-crypto@1.0.0.0 · 61 lines · 6 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/ppub.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
16
17# Scalars from bytes and public keys of src/crypto/secp256k1/ecdsa.bend
18# against spec/crypto/secp256k1/ecdsa.bend.
19
20# ---- scalars ----
21
22def 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>}:
23  match c:
24    case True{}:
25      PE.encode_compressed_v(one, h1, q, hq)
26    case False{}:
27      PE.encode_uncompressed_v(one, h1, q, hq)
28
29# [d] G
30def 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}:
31  %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}
32  %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}
33  {==}
34
35def 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}:
36  PM.mul_r(one, h1, d, P.g(), hd, PA.g_r(one, h1))
37
38def 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>>}:
39  match b:
40    case True{}:
41      %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>>}
42      %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>>}
43      {==}
44    case False{}:
45      {==}
46
47def 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>>}:
48  match a:
49    case True{}:
50      +hd = BY.of_be_limbs(one, h1, sk, ha)
51      %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>>}
52      %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>>}
53      %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>>}
54      pub_ok(one, h1, c, B.of_be(sk), hd, ES.scalar_ok(one, FS.value(one, B.of_be(sk))))
55    case False{}:
56      {==}
57
58# the SEC 1 public key of a secret key
59def 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>>}:
60  %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>>}
61  pub_len(one, h1, c, sk, CV.length_is(32n, sk), BL.hl_is(32n, sk))