proofs/crypto/secp256k1/semiring.bend

bend-collections-laws-crypto@1.0.0.0 · 31 lines · 7 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
4import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
5
6# The few semiring facts the rewrite generator (tools/generators/rw.py,
7# %norm) uses besides nat_algebra and width.
8
9def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:
10  {==}
11
12def zero_mul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
13  {==}
14
15def one_mul(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
16  NA.add_zero(x)
17
18def shift0(+x: Nat) -> {C.shift(0n, x) == x : Nat}:
19  {==}
20
21def mul_swap(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}:
22  %NA.mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
23  %NA.mul_assoc(b, a, c) : {Nat.mul(Nat.mul(a, b), c) == _ : Nat}
24  %NA.mul_comm(a, b) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(_, c) : Nat}
25  {==}
26
27def shift_shift(+j: Nat, +k: Nat, +x: Nat) -> {C.shift(j, C.shift(k, x)) == C.shift(Nat.add(j, k), x) : Nat}:
28  Equal.sym(Nat, C.shift(Nat.add(j, k), x), C.shift(j, C.shift(k, x)), WW.shift_comp(j, k, x))
29
30def succ_add(+k: Nat, +x: Nat) -> {Nat.add(k, x) == Nat.add(x, k) : Nat}:
31  NA.add_comm(k, x)