proofs/crypto/secp256k1/fprot.bend

bend-collections-laws-crypto@1.0.0.0 · 127 lines · 22 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/fprot.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
6
7# The field and scalar operations look at their arguments first (so that
8# the proof checker keeps them folded on unknown arguments); on any
9# arguments they are their unfolded *_u forms.
10
11def f_add_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.add(a, b) == F.add_b(a, b) : List<&2, Nat>}:
12  match a:
13    case Nil{}:
14      {==}
15    case x <> t:
16      {==}
17
18def f_add_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {F.add_b(a, b) == F.add_u(a, b) : List<&2, Nat>}:
19  match b:
20    case Nil{}:
21      {==}
22    case y <> u:
23      {==}
24
25def f_add(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.add(a, b) == F.add_u(a, b) : List<&2, Nat>}:
26  Equal.trans(List<&2, Nat>, F.add(a, b), F.add_b(a, b), F.add_u(a, b), f_add_a(a, b), f_add_b(a, b))
27
28def f_mul_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.mul(a, b) == F.mul_b(a, b) : List<&2, Nat>}:
29  match a:
30    case Nil{}:
31      {==}
32    case x <> t:
33      {==}
34
35def f_mul_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {F.mul_b(a, b) == F.mul_u(a, b) : List<&2, Nat>}:
36  match b:
37    case Nil{}:
38      {==}
39    case y <> u:
40      {==}
41
42def f_mul(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.mul(a, b) == F.mul_u(a, b) : List<&2, Nat>}:
43  Equal.trans(List<&2, Nat>, F.mul(a, b), F.mul_b(a, b), F.mul_u(a, b), f_mul_a(a, b), f_mul_b(a, b))
44
45def f_eq_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.eq(a, b) == F.eq_b(a, b) : Bool}:
46  match a:
47    case Nil{}:
48      {==}
49    case x <> t:
50      {==}
51
52def f_eq_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {F.eq_b(a, b) == L.eq(a, b) : Bool}:
53  match b:
54    case Nil{}:
55      {==}
56    case y <> u:
57      {==}
58
59def f_eq(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.eq(a, b) == L.eq(a, b) : Bool}:
60  Equal.trans(Bool, F.eq(a, b), F.eq_b(a, b), L.eq(a, b), f_eq_a(a, b), f_eq_b(a, b))
61
62def s_add_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.add(a, b) == S.add_b(a, b) : List<&2, Nat>}:
63  match a:
64    case Nil{}:
65      {==}
66    case x <> t:
67      {==}
68
69def s_add_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {S.add_b(a, b) == S.add_u(a, b) : List<&2, Nat>}:
70  match b:
71    case Nil{}:
72      {==}
73    case y <> u:
74      {==}
75
76def s_add(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.add(a, b) == S.add_u(a, b) : List<&2, Nat>}:
77  Equal.trans(List<&2, Nat>, S.add(a, b), S.add_b(a, b), S.add_u(a, b), s_add_a(a, b), s_add_b(a, b))
78
79def s_mul_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.mul(a, b) == S.mul_b(a, b) : List<&2, Nat>}:
80  match a:
81    case Nil{}:
82      {==}
83    case x <> t:
84      {==}
85
86def s_mul_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {S.mul_b(a, b) == S.mul_u(a, b) : List<&2, Nat>}:
87  match b:
88    case Nil{}:
89      {==}
90    case y <> u:
91      {==}
92
93def s_mul(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.mul(a, b) == S.mul_u(a, b) : List<&2, Nat>}:
94  Equal.trans(List<&2, Nat>, S.mul(a, b), S.mul_b(a, b), S.mul_u(a, b), s_mul_a(a, b), s_mul_b(a, b))
95
96def s_eq_a(a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.eq(a, b) == S.eq_b(a, b) : Bool}:
97  match a:
98    case Nil{}:
99      {==}
100    case x <> t:
101      {==}
102
103def s_eq_b(+a: List<&2, Nat>, b: List<&2, Nat>) -> {S.eq_b(a, b) == L.eq(a, b) : Bool}:
104  match b:
105    case Nil{}:
106      {==}
107    case y <> u:
108      {==}
109
110def s_eq(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {S.eq(a, b) == L.eq(a, b) : Bool}:
111  Equal.trans(Bool, S.eq(a, b), S.eq_b(a, b), L.eq(a, b), s_eq_a(a, b), s_eq_b(a, b))
112
113def f_neg(a: List<&2, Nat>) -> {F.neg(a) == F.neg_u(a) : List<&2, Nat>}:
114  {==}
115
116def s_neg(a: List<&2, Nat>) -> {S.neg(a) == S.neg_u(a) : List<&2, Nat>}:
117  {==}
118
119def s_reduce(xs: List<&2, Nat>) -> {S.reduce(xs) == S.reduce_u(xs) : List<&2, Nat>}:
120  {==}
121
122def lred(+c: List<&2, Nat>, +k: Nat, xs: List<&2, Nat>) -> {L.reduce(c, k, xs) == L.reduce_go(c, k, xs) : List<&2, Nat>}:
123  match xs:
124    case Nil{}:
125      {==}
126    case x <> t:
127      {==}