chore: audit Permutation argument 3

barretenberg/cpp/src/barretenberg/circuit_checker/ultra_circuit_builder_sort_permutation.test.cpp

@@ -30,13 +30,14 @@ TEST(UltraCircuitBuilder, NonTrivialTagPermutation)
     builder.create_add_gate({ a_idx, b_idx, builder.zero_idx(), fr::one(), fr::one(), fr::zero(), fr::zero() });
     builder.create_add_gate({ c_idx, d_idx, builder.zero_idx(), fr::one(), fr::one(), fr::zero(), fr::zero() });
 
-    builder.create_tag(1, 2);
-    builder.create_tag(2, 1);
+    auto first_tag = builder.get_new_tag();
+    auto second_tag = builder.get_new_tag();
+    builder.set_tau_transposition(first_tag, second_tag);
 
-    builder.assign_tag(a_idx, 1);
-    builder.assign_tag(b_idx, 1);
-    builder.assign_tag(c_idx, 2);
-    builder.assign_tag(d_idx, 2);
+    builder.assign_tag(a_idx, first_tag);
+    builder.assign_tag(b_idx, first_tag);
+    builder.assign_tag(c_idx, second_tag);
+    builder.assign_tag(d_idx, second_tag);
 
     EXPECT_TRUE(CircuitChecker::check(builder));
 
@@ -64,13 +65,14 @@ TEST(UltraCircuitBuilder, NonTrivialTagPermutationAndCycles)
     auto h_idx = builder.add_variable(c);
     builder.assert_equal(g_idx, h_idx);
 
-    builder.create_tag(1, 2);
-    builder.create_tag(2, 1);
+    auto first_tag = builder.get_new_tag();
+    auto second_tag = builder.get_new_tag();
+    builder.set_tau_transposition(first_tag, second_tag);
 
-    builder.assign_tag(a_idx, 1);
-    builder.assign_tag(c_idx, 1);
-    builder.assign_tag(e_idx, 2);
-    builder.assign_tag(g_idx, 2);
+    builder.assign_tag(a_idx, first_tag);
+    builder.assign_tag(c_idx, first_tag);
+    builder.assign_tag(e_idx, second_tag);
+    builder.assign_tag(g_idx, second_tag);
 
     builder.create_add_gate({ b_idx, a_idx, builder.zero_idx(), fr::one(), fr::neg_one(), fr::zero(), fr::zero() });
     builder.create_add_gate({ c_idx, g_idx, builder.zero_idx(), fr::one(), -fr::one(), fr::zero(), fr::zero() });
@@ -99,13 +101,14 @@ TEST(UltraCircuitBuilder, BadTagPermutation)
 
     EXPECT_TRUE(CircuitChecker::check(builder));
 
-    builder.create_tag(1, 2);
-    builder.create_tag(2, 1);
+    auto first_tag = builder.get_new_tag();
+    auto second_tag = builder.get_new_tag();
+    builder.set_tau_transposition(first_tag, second_tag);
 
-    builder.assign_tag(a_idx, 1);
-    builder.assign_tag(b_idx, 1);
-    builder.assign_tag(c_idx, 2);
-    builder.assign_tag(d_idx, 2);
+    builder.assign_tag(a_idx, first_tag);
+    builder.assign_tag(b_idx, first_tag);
+    builder.assign_tag(c_idx, second_tag);
+    builder.assign_tag(d_idx, second_tag);
 
     EXPECT_FALSE(CircuitChecker::check(builder));
 }

barretenberg/cpp/src/barretenberg/honk/composer/composer_lib.test.cpp

@@ -1,35 +1,30 @@
 #include "barretenberg/honk/composer/composer_lib.hpp"
 #include "barretenberg/flavor/ultra_flavor.hpp"
+#include "barretenberg/honk/composer/permutation_lib.hpp"
 #include "barretenberg/srs/factories/crs_factory.hpp"
 #include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp"
+#include "barretenberg/ultra_honk/ultra_honk.test.hpp"
 
 #include <array>
 #include <gtest/gtest.h>
 
 using namespace bb;
 
-class ComposerLibTests : public ::testing::Test {
+class ComposerLibTests : public UltraHonkTests<UltraFlavor> {
   public:
     using Flavor = UltraFlavor;
-    using FF = typename Flavor::FF;
-
-  protected:
-    static void SetUpTestSuite() { bb::srs::init_file_crs_factory(bb::srs::bb_crs_path()); }
+    using FF = Flavor::FF;
+    using Builder = UltraCircuitBuilder;
+    using Polynomial = Flavor::Polynomial;
 };
-
 /**
- * @brief A test to demonstrate that lookup read counts/tags are computed correctly for a simple 'hand-computable' case
- * using the uint32 XOR table
+ * @brief A test to demonstrate that lookup read counts/tags are computed correctly for a
+ * simple 'hand-computable' case using the uint32 XOR table
  *
  */
 TEST_F(ComposerLibTests, LookupReadCounts)
 {
-    using Builder = UltraCircuitBuilder;
-    using Flavor = UltraFlavor;
-    using FF = typename Flavor::FF;
-    using Polynomial = typename Flavor::Polynomial;
     auto UINT32_XOR = plookup::MultiTableId::UINT32_XOR;
-
     Builder builder;
 
     // define some very simply inputs to XOR
@@ -77,3 +72,41 @@ TEST_F(ComposerLibTests, LookupReadCounts)
         idx++;
     }
 }
+
+/**
+ * @brief Test that that if two distinct elements are given tags that are related by a transposition in tau, then the
+ * circuit fails.
+ *
+ */
+TEST_F(ComposerLibTests, TagCollisionFailure)
+{
+    {
+        Builder builder;
+
+        FF val_a = FF::random_element();
+        FF val_b = FF::random_element(); // Different value
+        ASSERT_FALSE(val_a == val_b);
+
+        auto a_idx = builder.add_variable(val_a);
+        auto b_idx = builder.add_variable(val_b);
+
+        auto first_tag = builder.get_new_tag();
+        auto second_tag = builder.get_new_tag();
+        builder.set_tau_transposition(first_tag, second_tag);
+        // Assign the same tag to both variables (which have different values)
+        // As we only have two witnesses, this forces a multiset-equality check `{val_a} == {val_b}`, which should fail.
+        builder.assign_tag(a_idx, first_tag);
+        builder.assign_tag(b_idx, second_tag);
+
+        // Use the variables in gates so they appear in the trace
+        builder.create_add_gate(
+            { a_idx, builder.zero_idx(), builder.zero_idx(), FF::one(), FF::zero(), FF::zero(), -val_a });
+        builder.create_add_gate(
+            { b_idx, builder.zero_idx(), builder.zero_idx(), FF::one(), FF::zero(), FF::zero(), -val_b });
+
+        // Add required pairing points for Ultra circuits
+        set_default_pairing_points_and_ipa_claim_and_proof(builder);
+
+        prove_and_verify(builder, /*expected_result=*/false);
+    }
+}

barretenberg/cpp/src/barretenberg/honk/composer/permutation_lib.hpp

@@ -47,11 +47,13 @@ struct cycle_node {
  *
  */
 struct Mapping {
-    std::shared_ptr<uint32_t[]> row_idx; // row idx of next entry in copy cycle
-    std::shared_ptr<uint8_t[]> col_idx;  // column idx of next entry in copy cycle
-    std::shared_ptr<bool[]> is_public_input;
-    std::shared_ptr<bool[]> is_tag; // is this element a tag,  (N.B. For each permutation polynomial (i.e., id_i or
-                                    // sigma_j), only one element per cycle is a tag.)
+    std::shared_ptr<uint32_t[]> row_idx;     // row idx of next entry in copy cycle
+    std::shared_ptr<uint8_t[]> col_idx;      // column idx of next entry in copy cycle
+    std::shared_ptr<bool[]> is_public_input; // if we are a sigma polynomial, is the current row a public input row?
+                                             // (always false for id polynomials.)
+    std::shared_ptr<bool[]>
+        is_tag; // is this element a tag,  (N.B. For each permutation polynomial (i.e., id_i or
+                // sigma_j), only one element per cycle is a tag. This follows the generalized permutation argument.)
     size_t _size = 0;
 
     Mapping() = default;
@@ -103,7 +105,7 @@ template <size_t NUM_WIRES> struct PermutationMapping {
                     // id polynomials
                     ids[col_idx].row_idx[idx] = row_idx;
                     ids[col_idx].col_idx[idx] = col_idx;
-                    ids[col_idx].is_public_input[idx] = false;
+                    ids[col_idx].is_public_input[idx] = false; // always false.
                     ids[col_idx].is_tag[idx] = false;
                 }
             }
@@ -115,19 +117,21 @@ using CyclicPermutation = std::vector<cycle_node>;
 
 namespace {
 
-static constexpr size_t PERMUTATION_POLY_START_INDEX =
+constexpr size_t PERMUTATION_POLY_START_INDEX =
     1; // start_index of the Sigma and ID polynomials, which are shiftable. (Note that they are never shifted.)
 
 /**
  * @brief Compute the permutation mapping
  *
- * @details Computes the mappings from which the sigma and ID polynomials can be computed. The output is proving-system
- * agnostic.
+ * @details Computes the mappings from which the sigma and ID polynomials can be computed, as specified by the
+ * Generalized Permutation argument. The output is proving-system agnostic.
  *
  * @param circuit_constructor
  * @param dyadic_size
  * @param wire_copy_cycles
  * @return PermutationMapping<Flavor::NUM_WIRES>
+ * @note This does not take into account the optimization for public inputs, a.k.a. the "public inputs delta"; it purely
+ * reflects the actual copy cycles.
  */
 template <typename Flavor>
 PermutationMapping<Flavor::NUM_WIRES> compute_permutation_mapping(
@@ -182,7 +186,9 @@ PermutationMapping<Flavor::NUM_WIRES> compute_permutation_mapping(
     }
 
     // Add information about public inputs so that the cycles can be altered later; See the construction of the
-    // permutation polynomials for details.
+    // permutation polynomials for details. This _only_ effects sigma_0, the 0th sigma polynomial, as the structure of
+    // the algorithm only requires modifying sigma_0(i) where i is a public input row. (Note that at such a row, the
+    // non-zero wire values are in w_l and w_r, and both of them contain the public input.)
     const auto num_public_inputs = static_cast<uint32_t>(circuit_constructor.num_public_inputs());
 
     auto pub_inputs_offset = circuit_constructor.blocks.pub_inputs.trace_offset();
@@ -237,20 +243,29 @@ void compute_honk_style_permutation_lagrange_polynomials_from_mapping(
                 const auto& current_row_idx = permutation_mappings[wire_idx].row_idx[idx];
                 const auto& current_col_idx = permutation_mappings[wire_idx].col_idx[idx];
                 const auto& current_is_tag = permutation_mappings[wire_idx].is_tag[idx];
-                const auto& current_is_public_input = permutation_mappings[wire_idx].is_public_input[idx];
+                const auto& current_is_public_input =
+                    permutation_mappings[wire_idx].is_public_input[idx]; // this is only `true` for sigma polynomials,
+                                                                         // it is always false for the ID polynomials.
                 if (current_is_public_input) {
-                    // We intentionally want to break the cycles of the public input variables.
-                    // During the witness generation, the left and right wire polynomials at idx i contain the i-th
-                    // public input. Let n = SEPARATOR. The CyclicPermutation created for these variables
-                    // always starts with (i) -> (n+i), followed by the indices of the variables in the "real" gates. We
-                    // make i point to -(i+1), so that the only way of repairing the cycle is add the mapping
-                    //  -(i+1) -> (n+i)
-                    // These indices are chosen so they can easily be computed by the verifier. They can expect
-                    // the running product to be equal to the "public input delta" that is computed
-                    // in <honk/utils/grand_product_delta.hpp>
+                    // We intentionally want to break the cycles of the public input variables as an optimization.
+                    // During the witness generation, both the left and right wire polynomials (w_l and w_r
+                    // respectively) at row idx i contain the i-th public input. Let n = SEPARATOR. The initial
+                    // CyclicPermutation created for these variables copy-constrained to the ith public input therefore
+                    // always starts with (i) -> (n+i), followed by the indices of the variables in the "real" gates
+                    // (i.e., the gates not merely present to set-up inputs).
+                    //
+                    // We change this and make i point to -(i+1). This choice "unbalances" the grand product argument,
+                    // so that the final result of the grand product is _not_ 1. These indices are chosen so they can
+                    // easily be computed by the verifier (just knowing the public inputs), and this algorithm
+                    // constitutes a specification of the "permutation argument with public inputs" optimization due to
+                    // Gabizon and Williamson. The verifier can expect the final product to be equal to the "public
+                    // input delta" that is computed in <honk/library/grand_product_delta.hpp>.
                     current_permutation_poly.at(poly_idx) = -FF(current_row_idx + 1 + SEPARATOR * current_col_idx);
                 } else if (current_is_tag) {
-                    // Set evaluations to (arbitrary) values disjoint from non-tag values
+                    // Set evaluations to (arbitrary) values disjoint from non-tag values. This is for the
+                    // multiset-equality part of the generalized permutation argument, which requires auxiliary values
+                    // which have not been used as indices. In particular, these are the actual tags assigned to the
+                    // cycle.
                     current_permutation_poly.at(poly_idx) = SEPARATOR * Flavor::NUM_WIRES + current_row_idx;
                 } else {
                     // For the regular permutation we simply point to the next location by setting the

barretenberg/cpp/src/barretenberg/honk/library/grand_product_delta.hpp

@@ -13,11 +13,10 @@ namespace bb {
 /**
  * @brief Compute the correction term for the permutation argument.
  *
- * @tparam Field
+ * @tparam Flavor
  * @param public_inputs x₀, ..., xₘ₋₁ public inputs to the circuit
  * @param beta random linear-combination term to combine both (wʲ, IDʲ) and (wʲ, σʲ)
  * @param gamma Schwartz-Zippel random evaluation to ensure ∏ᵢ (γ + Sᵢ) = ∏ᵢ (γ + Tᵢ)
- * @param domain_size Total number of rows required for the circuit (power of 2)
  * @param offset Extent to which PI are offset from the 0th index in the wire polynomials, for example, due to inclusion
  * of a leading zero row or Goblin style ECC op gates at the top of the execution trace.
  * @return Field Public input Δ
@@ -28,9 +27,9 @@ typename Flavor::FF compute_public_input_delta(std::span<const typename Flavor::
                                                const typename Flavor::FF& gamma,
                                                const typename Flavor::FF& offset = 0)
 {
-    using Field = typename Flavor::FF;
-    Field numerator = Field(1);
-    Field denominator = Field(1);
+    using FF = typename Flavor::FF;
+    FF numerator = FF(1);
+    FF denominator = FF(1);
 
     // Let m be the number of public inputs x₀,…, xₘ₋₁.
     // Recall that we broke the permutation σ⁰ by changing the mapping
@@ -45,8 +44,10 @@ typename Flavor::FF compute_public_input_delta(std::span<const typename Flavor::
     //  -----------------------  =  ------------------------
     //   ∏ᵢ (γ + W⁰ᵢ + β⋅σ⁰ᵢ )        ∏ᵢ (γ + xᵢ - β⋅(i+1) )
 
-    // At the start of the loop for each xᵢ where i = 0, 1, …, m-1,
-    // we have
+    // The RHS is often referred to as the "grand product delta". Note that the products on the RHS is only over the
+    // public input indices, while the products on the LHS are over the entire circuit.
+    //
+    // At the start of the loop for each xᵢ where i = 0, 1, …, m-1, we have
     //      numerator_acc   = γ + β⋅(n+i) = γ + β⋅n + β⋅i
     //      denominator_acc = γ - β⋅(1+i) = γ - β   - β⋅i
     // at the end of the loop, add and subtract β to each term respectively to
@@ -57,9 +58,9 @@ typename Flavor::FF compute_public_input_delta(std::span<const typename Flavor::
 
     // Using n = SEPARATOR ensures that the evaluations of `id_i` (`sigma_i`) and `id_j`(`sigma_j`) polynomials on the
     // boolean hypercube do not intersect for i != j.
-    const Field SEPARATOR(PERMUTATION_ARGUMENT_VALUE_SEPARATOR);
-    Field numerator_acc = gamma + (beta * (SEPARATOR + offset));
-    Field denominator_acc = gamma - beta * (offset + 1);
+    const FF SEPARATOR(PERMUTATION_ARGUMENT_VALUE_SEPARATOR);
+    FF numerator_acc = gamma + (beta * (SEPARATOR + offset));
+    FF denominator_acc = gamma - beta * (offset + 1);
 
     for (size_t i = 0; i < public_inputs.size(); i++) {
         numerator *= (numerator_acc + public_inputs[i]);     // γ + xᵢ + β(n+i)