1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/ppub.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/field.bend as FS 4 import ../../../spec/crypto/secp256k1/curve.bend as CV 5 import ../../../spec/crypto/secp256k1/ecdsa.bend as ES 6 import ../../../src/crypto/secp256k1/bytes.bend as B 7 import ../../../src/crypto/secp256k1/point.bend as P 8 import ../../../src/crypto/secp256k1/ecdsa.bend as E 9 import ./bytes.bend as BY 10 import ./point.bend as PT 11 import ./pmul.bend as PM 12 import ./paff.bend as PA 13 import ./penc.bend as PE 14 import ./blist.bend as BL 15 import ./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 22 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>}: 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 30 def 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 35 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}: 36 PM.mul_r(one, h1, d, P.g(), hd, PA.g_r(one, h1)) 37 38 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>>}: 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 47 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>>}: 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 59 def 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))