1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/fprot.src; edit the .src
2	import Base
3	import ../../../src/crypto/secp256k1/limbs.bend as L
4	import ../../../src/crypto/secp256k1/field.bend as F
5	import ../../../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	
11	def 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	
18	def 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	
25	def 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	
28	def 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	
35	def 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	
42	def 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	
45	def 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	
52	def 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	
59	def 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	
62	def 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	
69	def 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	
76	def 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	
79	def 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	
86	def 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	
93	def 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	
96	def 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	
103	def 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	
110	def 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	
113	def f_neg(a: List<&2, Nat>) -> {F.neg(a) == F.neg_u(a) : List<&2, Nat>}:
114	  {==}
115	
116	def s_neg(a: List<&2, Nat>) -> {S.neg(a) == S.neg_u(a) : List<&2, Nat>}:
117	  {==}
118	
119	def s_reduce(xs: List<&2, Nat>) -> {S.reduce(xs) == S.reduce_u(xs) : List<&2, Nat>}:
120	  {==}
121	
122	def 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	      {==}