proofs/crypto/secp256k1/pscal.bend

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

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pscal.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fprot.bend as FR
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
16
17# Scalars from bytes: x mod n for 16 limbs, the hash of a message as a
18# scalar, and 1 <= x < n.
19
20def scalar_ok_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>) -> {E.scalar_ok(x) == ES.scalar_ok(one, FS.value(one, x)) : Bool}:
21  %Equal.sym(Bool, S.is_zero(x), Nat.is_eq(FS.value(one, x), 0n), FW.is_zero_s(one, h1, x)) : {Bool.and(Bool.not(_), S.lt_n(x)) == Bool.and(Bool.not(Nat.is_eq(FS.value(one, x), 0n)), Nat.is_lt(FS.value(one, x), FS.order(one))) : Bool}
22  %Equal.sym(Bool, S.lt_n(x), Nat.is_lt(FS.value(one, x), FS.order(one)), FW.lt_n_s(one, h1, x)) : {Bool.and(Bool.not(Nat.is_eq(FS.value(one, x), 0n)), _) == Bool.and(Bool.not(Nat.is_eq(FS.value(one, x), 0n)), Nat.is_lt(FS.value(one, x), FS.order(one))) : Bool}
23  {==}
24
25# a 16-limb value is below 2^512
26def ev512(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
27  +t = C.shift(256n, one)
28  SO.lt3(one, h1, LV.ev(x), N.lt_le_trans(LV.ev(x), t, Nat.add(t, Nat.add(t, t)), SO.tt_lt(one, h1, x, hx), N.le_add_right(t, Nat.add(t, t))))
29
30# x mod n for a 16-limb x
31def sred_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {FS.value(one, S.reduce(x)) == Nat.mod(FS.value(one, x), FS.order(one)) : Nat}:
32  %Equal.sym(List<&2, Nat>, S.reduce(x), S.reduce_u(x), FR.s_reduce(x)) : {FS.value(one, _) == Nat.mod(FS.value(one, x), FS.order(one)) : Nat}
33  %Equal.sym(Nat, FS.value(one, S.reduce_u(x)), Nat.mod(LV.ev(x), FS.order(one)), SO.red_v(one, h1, x, ev512(one, h1, x, hx))) : {_ == Nat.mod(FS.value(one, x), FS.order(one)) : Nat}
34  %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {Nat.mod(LV.ev(x), FS.order(one)) == Nat.mod(_, FS.order(one)) : Nat}
35  {==}
36
37def sred_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.reduce(x)) == True{} : Bool}:
38  %Equal.sym(List<&2, Nat>, S.reduce(x), S.reduce_u(x), FR.s_reduce(x)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool}
39  SO.red_r(one, h1, x, ev512(one, h1, x, hx))
40
41def hash_v(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hl: {B.has_len(32n, h) == True{} : Bool}) -> {FS.value(one, E.hash_scalar(h)) == ES.hash_scalar(one, h) : Nat}:
42  %Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(h))), Nat.mod(FS.value(one, B.of_be(h)), FS.order(one)), sred_v(one, h1, B.of_be(h), BY.of_be_limbs(one, h1, h, hl))) : {_ == Nat.mod(CV.os2ip(h), FS.order(one)) : Nat}
43  %Equal.sym(Nat, FS.value(one, B.of_be(h)), CV.os2ip(h), BY.of_be_value(one, h1, h)) : {Nat.mod(_, FS.order(one)) == Nat.mod(CV.os2ip(h), FS.order(one)) : Nat}
44  {==}
45
46def hash_r(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hl: {B.has_len(32n, h) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), E.hash_scalar(h)) == True{} : Bool}:
47  sred_r(one, h1, B.of_be(h), BY.of_be_limbs(one, h1, h, hl))
48
49# ---- public keys ----