Especificar con pre, poscondición, declaración de constantes y variables los siguientes problemas: a) Dados los arreglos a y b determinar si todos los elementos de a son mayores a exactamente dos elementos de b. Solución posible Const N: Int; Const M: Int; Var a: array $[0,N)$ of Num; Var b: array $[0, M)$ of Num; Var r: Bool; ${P: N\geq 0 \land M\geq 0}$

Especificar con pre, poscondición, declaración de constantes y variables los siguientes programas: a) Dados dos arreglos A y B decir si existe un elemento de A que sea igual al promedio de dos elementos de B. Solución posible: Const : N Int Const: M Int var A: array $[0,N)$ of Num var B: array $[0,M)$ of Num Var r: Bool

Especificar los siguientes programas imperativos: a) Dados los arreglos A y B, determina si todos los elementos de A son mayores a todos los elementos de B. Solución posible: Const : N Int Const: M Int var A: array $[0,N)$ of Num var B: array $[0,M)$ of Num r: Bool

We thank the reviewers for helpful comments and detailed inspection. All concerns and minor typos will be addressed. We are especially thankful for the presentation suggestion of Reviewer A for introduction and Section 5, and for the detailed input on the Definition 5 and suggestions for technical overview from Reviewer B, we will take them all in account for the final version. General Comments --Comparison with previous work-- We recall the difference from O(m^2) in Caulk+ to O(m) in Baloo is in group operations for the prover, while in the field asymptotic efficiency is the same. In Flookup techniques are very different and the construction uses a non-homomorphic commitment to the big table; this makes it complicated to use it as a building block in many protocols, which is one of the goals for Baloo. An extra discussion is devoted to EFG22 as it is the only one that, while having homomorphic commitments, outperforms Baloo. We have only compared concrete performance with Caulk because it is, to the best of our knowledge, the only protocol that has an implementation publicly available. It is in our interests to compare with all existing constructions. EFG22: We apologize as there is a typo in the table on the performance of cq, where it says O(m log^2 m) should be O(m log m). Please note the reported efficiency in the paragraph called "Concurrent work" is the correct one. We are especially interested in a comparison with EFG22, as the prover performance only differs asymptotically on a log(m) factor for field operations, while Baloo offers an extra feature. Namely, in cq two lookup tables $\vec a=(a_1, a_3, a_7, a_3)$ and $\vec a'=(a_7, a_1, a_3, a_3)$ are indistinguishable. That is, given table $\vec t$, the prover in cq commits to the elements taken from the public table to construct the lookup, and its repetitions, but not to the order. In Baloo, as we use a matrix to construct the lookup from the public table, the prover commits to the elements, the repetitions, and the order as well.The difference above implies Baloo can be used for proving "repeated" lookups, meaning the same lookup operation is applied to one or two different tables, and also for the case where the lookup is made public (either because matrix $\matrix M$ is public or published by the Prover after the interaction). The latter is the case in applications such as memory access or subset opening, where the system needs to keep track of the order of the elements in all tables. Reviewer A

$P(X,Y)=\sum_{i=1}^m \lambda_i(X)\mu_i(Y)$, where ${\lambda_i(X)}{i=1}^m$ is the set of interpolation polynomials for the subgroup $\mathbb{H}={1, \omega, \ldots, \omega^{m-1}}$ of size $m$, while ${\mu_i(X)}{i=1}^M$ interpolate the subgroup $\mathbb{V}={1, \nu, \ldots, \nu^{M-1}}$, M>m. Is $\mathbb{H}\subset\mathbb{V}??$ If $\mathbb{H}\subset\mathbb{V}$ then as $$ \lambda_i(X) = \frac{\omega^i(X^m-1)}{m(X-\omega^i)}; \quad \mu_j(X) = \frac{\nu^j(X^M-1)}{M(X-\nu^j)} $$ we have $$ \omega = \nu^t