add an FRI verifier summary in the commentary

commentary/FRI.md

@@ -230,6 +230,20 @@ As what we really want to compute is $\sum_k \beta^k P_k(x_0^8)$, we can see tha
 
 This can be reinterpreted as interpolating a degree `arity-1` polynomial from these values, and evaluating it at $\beta$, and indeed this is how Plonky2 implements it.
 
+### FRI verifier summary
+
+So what does the verifier needs to check at the end?
+
+- check if the public parameters match the proof "shape" (arities, number of query rounds, Merkle cap sizes, etc)
+- check the proof-of-work response
+- then for each query round:
+    - check the initial tree Merkle proofs against the 4 commitments (constants, witness, partial products and quotient)
+    - compute the evaluation of the combined polynomial from these values (a single row) at the query location
+    - for each folding step:
+        - check the coset opening proof against the corresponding commit phase Merkle cap
+        - check if the right element in the coset values matches the evaluation coming from the previous step (in the very first step, against the above compute value)
+        - calculate the folded value, and pass it to the next step
+    - check the final folded value against the evaluation of the final polynomial
 
 ### FRI verification cost
 

commentary/Lookups.md

@@ -132,7 +132,7 @@ Lookup tables are encoded in several `LookupTable` gates, which are just below e
             +---------------+
             |     ....      |
 
-Both type of gates are padded if necessary to get full rows. The `Lookup` gates are padded with the first entry in the corresponding table, while the `LookupTable` gates are padded with zeros (which is actually a soundness bug, as now you can prove that `(0,0)` is an element of any table whose length is not divisible by 26).
+Both type of gates are padded if necessary to get full rows. The `Lookup` gates are padded with the first entry in the corresponding table, while the `LookupTable` gates used to be padded with zeros (which was actually a soundness bug, as you could prove that `(0,0)` is an element of any table whose length is not divisible by 26), but this was fixed in [commit 091047f](https://github.com/0xPolygonZero/plonky2/commit/091047f7f10cae082716f3738ad59a583835f7b6), and now that's also padded by the first entry.
 
 
 ### Lookup selectors