Add phantom permutation in `std::protocols::permutation::permutation(…

…)` + change tests (#2069)

With this PR, `std::protocols::permutation::permutation()` adds a
phantom permutation as well, making witgen work when using it.

Also, I changed the tests to be analogous to recent changes to the
`lookup_via_challenges` test:
- The `_ext` variant is removed, since we automatically run the
extension field variant on Goldilocks (which is tested)
- The example itself is more realistic, in this case it emulates a block
machine connected via a permutation.

pipeline/tests/powdr_std.rs

@@ -172,13 +172,6 @@ fn permutation_via_challenges() {
     test_plonky3_with_backend_variant::<GoldilocksField>(f, vec![], BackendVariant::Monolithic);
 }
 
-#[test]
-fn permutation_via_challenges_ext() {
-    let f = "std/permutation_via_challenges_ext.asm";
-    test_halo2(make_simple_prepared_pipeline(f));
-    test_plonky3_with_backend_variant::<GoldilocksField>(f, vec![], BackendVariant::Monolithic);
-}
-
 #[test]
 fn lookup_via_challenges() {
     let f = "std/lookup_via_challenges.asm";

std/protocols/lookup.asm

@@ -58,9 +58,6 @@ let compute_next_z: Fp2<expr>, Fp2<expr>, Fp2<expr>, Constr, expr -> fe[] = quer
 /// Transforms a single lookup constraint to identity constraints, challenges and
 /// higher-stage witness columns.
 /// Use this function if the backend does not support lookup constraints natively.
-/// WARNING: This function can currently not be used multiple times since
-/// the used challenges would overlap.
-/// TODO: Implement this for an array of constraints.         
 let lookup: Constr -> () = constr |lookup_constraint| {
     std::check::assert(required_extension_size() <= 2, || "Invalid extension size");
     // Alpha is used to compress the LHS and RHS arrays.

std/protocols/permutation.asm

@@ -17,6 +17,7 @@ use std::math::fp2::required_extension_size;
 use std::math::fp2::needs_extension;
 use std::protocols::fingerprint::fingerprint;
 use std::utils::unwrap_or_else;
+use std::constraints::to_phantom_permutation;
 
 let unpack_permutation_constraint: Constr -> (expr, expr[], expr, expr[]) = |permutation_constraint| match permutation_constraint {
     Constr::Permutation((lhs_selector, rhs_selector), values) => (
@@ -54,9 +55,6 @@ let compute_next_z: Fp2<expr>, Fp2<expr>, Fp2<expr>, Constr -> fe[] = query |acc
 };
 
 /// Returns constraints that enforce that lhs is a permutation of rhs
-/// WARNING: This function can currently not be used multiple times since
-/// the used challenges would overlap
-/// TODO: Implement this for an array of constraints
 ///
 /// # Implementation:
 /// This function implements a permutation argument described e.g. in
@@ -110,6 +108,9 @@ let permutation: Constr -> () = constr |permutation_constraint| {
     is_first * acc_2 = 0;
     constrain_eq_ext(update_expr, from_base(0));
 
+    // Add an annotation for witness generation
+    to_phantom_permutation(permutation_constraint);
+
     // In the extension field, we need a prover function for the accumulator.
     if needs_extension() {
         // TODO: Helper columns, because we can't access the previous row in hints

test_data/std/permutation_via_challenges.asm

@@ -1,24 +1,18 @@
-use std::prelude::Query;
-use std::convert::fe;
 use std::protocols::permutation::permutation;
-use std::math::fp2::from_base;
-use std::prover::challenge;
 
 machine Main with degree: 8 {
 
-    col fixed first_four = [1, 1, 1, 1, 0, 0, 0, 0];
+    col fixed x = [0, 0, 1, 2, 3, 4, 5, 6];
+    col witness y;
 
-    // Two pairs of witness columns, claimed to be permutations of one another
-    // (when selected by first_four and (1 - first_four), respectively)
-    col witness a1, a2, b1, b2;
-    query |i| {
-        std::prover::provide_value(a1, i, fe(i));
-        std::prover::provide_value(a2, i, fe(i + 42));
-        std::prover::provide_value(b1, i, fe(7 - i));
-        std::prover::provide_value(b2, i, fe(7 - i + 42));
-    };
+    // A small block machine that computes f(x) = x + 42;
+    col witness sub_x, sub_y, sub_sel;
+    sub_y = sub_x + 42;
 
-    let permutation_constraint = first_four $ [a1, a2] is (1 - first_four) $ [b1, b2];
+    // Currently, witgen fails if the block machine has just enough rows to
+    // fit all the blocks, so let's not have a call in the last row.
+    col fixed sel = [1, 1, 1, 1, 1, 1, 1, 0];
 
-    permutation(permutation_constraint);
-}
+    // Add the permutation constraints
+    permutation(sel $ [x, y] is sub_sel $ [sub_x, sub_y]);
+}