[docs] Port the example that @ax0 told me months ago about a theorem-ish perspective on predicates, and updates the signature section adding a note (& references) on the current signature scheme. (#443)

* Port the example that @ax0 told me months ago about a theorem-ish perspective on predicates, and updates the signature section adding a note (& references) on the current signature scheme.

* apply review corrections from @ed255

* update example with @artwyman IsComposite suggestion & transitive_eq example

book/src/SUMMARY.md

@@ -14,7 +14,7 @@
 - [Deductions](./deductions.md)
   - [Statements](./statements.md)
   - [Operations](./operations.md)
-    - [Simple example](./simpleexample.md)
+  - [Simple example](./simpleexample.md)
   - [Custom statements and custom operations](./custom.md)
     - [Defining custom predicates](./custompred.md)
     - [Custom statement example](./customexample.md)

book/src/signature.md

@@ -1,11 +1,16 @@
 # Signature
 
 
-Current signature scheme used is proof-based signatures using Plonky2 proofs, following [https://eprint.iacr.org/2024/1553](https://eprint.iacr.org/2024/1553) and [https://jdodinh.io/assets/files/m-thesis.pdf](https://jdodinh.io/assets/files/m-thesis.pdf). This comes from [Polygon Miden's RPO STARK-based](https://github.com/0xPolygonMiden/crypto/blob/d2a67396053fded90ec72690404c8c7728b98e4e/src/dsa/rpo_stark/signature/mod.rs#L129) signatures.
+For POD2 signatures, we use [Schnorr](https://en.wikipedia.org/wiki/Schnorr_signature) signature over the [EcGFp5 curve](https://eprint.iacr.org/2022/274).
-
-In future iterations we may replace it by other signature schemes (either elliptic curve based scheme on a Golilocks-prime friendly curve, or a lattice based scheme).
 
 
+## Older version
+
+The previously used signature scheme was proof-based signatures using Plonky2 proofs, following [https://eprint.iacr.org/2024/1553](https://eprint.iacr.org/2024/1553) and [https://jdodinh.io/assets/files/m-thesis.pdf](https://jdodinh.io/assets/files/m-thesis.pdf). This came from [Polygon Miden's RPO STARK-based](https://github.com/0xPolygonMiden/crypto/blob/d2a67396053fded90ec72690404c8c7728b98e4e/src/dsa/rpo_stark/signature/mod.rs#L129) signatures.
+
+This was replaced by the elliptic curve Schnorr signature presented above, keeping the description here in case it were useful in the future.
+
+The scheme was as follows:
 
 ### generate_params()
 $pp$: plonky2 circuit prover params<br>
@@ -36,6 +41,6 @@ $pk \stackrel{!}{=} H(sk)$<br>
 $s \stackrel{!}{=} H(pk, m)$
 
 
-<br><br>
+<br>
 
 [^1]: The [2024/1553 paper](https://eprint.iacr.org/2024/1553) uses $pk:=H(sk||0^4)$ to have as input (to the hash) 8 field elements, to be able to reuse the same instance of the RPO hash as the one they use later in the signature (where it hashes 8 field elements).

book/src/simpleexample.md

@@ -145,3 +145,57 @@ eth_friend(?1, ?2, ?3, ?4) = and<
     Equal(?5["attestation"], ?3[?4])
 >
 ```
+
+## Another perspective
+When working with statements and operations, it might be useful to see them from another perspective:
+
+- A *predicate* is a relation formula, which when filled with values becomes a
+  *statement*.
+- A *statement* can be seen as the *constraints* of a traditional zk-circuit,
+  which can be true or false.
+- An *operation* comprises the deduction rules, which are rules used to deduce
+  new statements from previous statements or used to construct new statements
+  from values.
+
+$$
+predicate \cong circuit/relation~to~be~fulfilled\\
+statement \cong constraints~filled~with~the~witness\\
+operations \cong deduction~rules
+$$
+
+
+For example,
+- `Equal` for integers is a *predicate*
+- `st_1 = Equal(A, B)` is a *statement*
+- `st_2 = Equal(B, C)` is a *statement*
+- `st_3 = TransitiveEqualFromStatements(st_1, st_2)` is an *operation*, which yields the statement `st_3 = Equal(A, C)`
+
+
+
+
+<div style="display:flex;">
+<div style="padding:10px;max-width:50%; border-right:1px solid #ccc;">
+    
+So, for example, for the given predicate:
+
+```
+IsComposite(n, private: a, b) = AND(
+  ProductOf(n, a, b)
+  GtFromEntries(a, 1)
+  GtFromEntries(b, 1)
+)
+```
+
+</div>
+<div style="padding:10px;max-width:45%;">
+    
+We can view it as:
+
+The *statement* `IsComposite(n)` is `true` if and only if $\exists$ `n`, `a`, `b`
+ such that the following statements hold:
+- $n = a \cdot b$
+- $a > 1$
+- $b > 1$
+
+</div>
+</div>