halo2 backend #151

leonardoalt · 2023-04-06T15:24:09Z

Extracted from the rest of #102. The other PR got a bit too complicated to rebase onto main because of the amount of changes in the main branch and the merge commits into the feature branch.

The author credits are kept in this PR.

Notes from @Schaeff:

the number of required extra rows is not trivial to calculate and seems to depend on the exact Halo2 configuration. Doubling the table size seems fine for this PR.
This PR removes the wrapping behavior. This means that if this is merged, the first row is not constrained together with the last row. Moreover, witness generation does not use wrapping logic.
This PR removes the requirement on the number of rows to be a power of two. This can be enforced by the backend instead: Halo2 just extends to the next power of two (if there is enough space) and say estark should throw.

src/halo2/circuit_data.rs

src/halo2/circuit_builder.rs

src/bin/compiler.rs

src/halo2/circuit_builder.rs

chriseth · 2023-04-07T09:04:37Z

src/halo2/circuit_builder.rs

+    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |
+    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |>  witness + fixed  2^(k-1)
+    // |  ...             |   ...        |      ...      |   ...            |  |
+    // |  bla_bla_bla     |    1         |       0       |   bla_bla_bla    | /     <- __enable_next == 0 since there's no state transition


Do we need this mechanism now?

HALO2 contains rows that are "poisoned" and are unusable, and PIL/zkWASM does not know about this fact, I have to activate polinomials on usable rows.

chriseth · 2023-04-07T09:06:55Z

src/halo2/circuit_builder.rs

+                .selector
+                .clone()
+                .map_or(Expr::Const(BigUint::one()), |expr| {
+                    expression_2_expr(&cd, &expr, int_to_field).0


Why can we ignore the fact that they contain rotations for plookups?

expression_2_expr takes care about rotations and are used in both left and right expressions.
But probably are you talking about something else..

leonardoalt · 2023-04-07T10:50:45Z

@adria0 I moved the Halo2 PR here because the other one became too complicated to rebase after a lot of changes to main. Chris has some questions above that I can't answer myself, could you answer those? Thanks!

leonardoalt · 2023-04-07T11:02:55Z

Just pushed the changes to the review comments I could fix.

chriseth · 2023-04-07T11:15:17Z

@adria0 I still don't fully understand the enable_next mechanism. Is it true that this PR removes any constraint that connects the last and the first row? Does this allow invalid proofs to be verified if they rely on that property?

chriseth · 2023-04-07T11:19:02Z

If yes, we could check if we rely on such a wrap-around property.

leonardoalt · 2023-04-07T11:24:00Z

If yes, we could check if we rely on such a wrap-around property.

We do on the "binary" state machine (for the FACTOR and input byte polys)

adria0 · 2023-04-07T11:33:19Z

BTW,

@adria0 I still don't fully understand the enable_next mechanism. Is it true that this PR removes any constraint that connects the last and the first row? Does this allow invalid proofs to be verified if they rely on that property?

Oh, yes, you're right on this @chriseth, since last rows are unusable in HALO2 👍

adria0 · 2023-04-07T11:38:07Z

BTW, this set_field_mod is really terrible and can break tests when executed in multithread.
For HALO2 tests, I'm going to change to use a ReentrantMutex<RefCell<BigInt>> that is still a patch but just a little less 😅

pub fn with_field_mod<F: FnOnce()>(n: BigInt, f: F) {
    let _ = ReentrantMutexGuard::map((*FIELD_MOD).lock(), |field_mod| {
        let previous = field_mod.borrow().clone();
        *field_mod.borrow_mut() = n;
        f();
        *FIELD_MOD.lock().borrow_mut() = previous;
        &()
    });
}

halo2/src/mock_prover.rs

chriseth · 2023-05-19T09:10:09Z

executor/src/witgen/mod.rs

@@ -118,12 +118,6 @@ pub fn generate<'a, T: FieldElement>(
            values[col].1.push(v);
        }
    }
-    for (col, v) in generator.compute_next_row(0).into_iter().enumerate() {


I think we should still check it, because halo is not the only backend.

Maybe the halo2 backend should not even modify the pil but instead only check that the last witness rows are free. Unconstraining the last rows could be an additional step.

We need to make all the compiler built-in stuff independent from wrapping

Should this be brought back based on the comments from @chriseth ?

If we bring it back, then we are requiring a halo2 program to have correct wrapped values, which it does not need to have. It's estark leaking onto halo2.

If we keep it out, we allow an estark program to have incorrect wrapped values, which will fail in estark. It's estark being stricter than powdr.

I prefer the latter until we solve #300 more cleanly.

Can we simply use this as a flag that is returned from witgen?

executor/src/witgen/generator.rs

chriseth · 2023-05-22T15:02:23Z

powdr_cli/src/main.rs

@@ -82,6 +87,19 @@ enum Commands {
        force: bool,
    },

+    /// Apply the Halo2 workflow on an input file and prover values.


In addition to that, shouldn't we also have an option to create the proof for all the other subcommands that perform witness generation?

Happy to add that in another PR

powdr_cli/src/main.rs

chriseth · 2023-05-22T15:06:09Z

number/src/serialize.rs

+    degree: DegreeType,
+    polys: &Vec<(&str, Vec<T>)>,
+) {
+    let width = f32::ceil(T::modulus().to_arbitrary_integer().bits() as f32 / 64f32) as usize * 8;


Why is this a multiple of 64 bits?

So this is a bit hacky but basically field elements are stored as arrays of u64, so this line gets the number of bytes to read for one field element.

chriseth · 2023-05-22T15:09:20Z

halo2/src/mock_prover.rs

+    // double the row count in order to make space for the cells introduced by the backend
+    // TODO: use a precise count of the extra rows needed to avoid using so many rows
+
+    let k = 1 + f32::log2(circuit.plaf.info.num_rows as f32).ceil() as u32;


Do we really need to convert to floating point just so that we have a ceil function? (also at other places)

Oh and can you use a descriptive name instead of k please?

chriseth · 2023-05-22T15:13:32Z

halo2/src/circuit_builder.rs

+    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |
+    // |  bla_bla_bla     |    1         |       1       |   bla_bla_bla    |  |>  witness + fixed  2^(k-1)
+    // |  ...             |   ...        |      ...      |   ...            |  |
+    // |  bla_bla_bla     |    1         |       0       |   bla_bla_bla    | /     <- __enable_next == 0 since there's no state transition


Could we fix this so that __enable_next has the same number above and below the ...? It's not clear when the transition from 1 to 0 happens.

It should be clearer now

chriseth · 2023-05-22T15:15:46Z

halo2/src/circuit_builder.rs

+    PlafH2Circuit { plaf, wit }
+}
+
+fn expression_2_expr<T: FieldElement>(


Please document the bool return value

We could also use contains_next_ref from the witgen utils.

done, I moved contains_next_ref (and similar functions) to an impl on Expression and used that

halo2/src/circuit_builder.rs

leonardoalt · 2023-05-23T19:48:55Z

executor/src/witgen/generator.rs

-        // Identity check failure on the first row is not fatal. We will proceed with
-        // "unknown", report zero and re-check the wrap-around against the zero values at the end.
-        if identity_failed && next_row != 0 {
+        if identity_failed {


What's the effect of this change? Is next_row expected to never be 0?

No: before this change, as far as I understand a failed identity on the first row was somehow not an issue.
I suspect this change is correct even outside the context of this PR, because since we introduced the EvalResult I can't see how we can recover from a failed identity (the message below should also be adjusted).

powdr_cli/src/main.rs

halo2/src/mock_prover.rs

halo2/src/circuit_builder.rs

leonardoalt

As the original author of the PR I actually can't approve it, but lgtm!
Maybe @chriseth can take another look and approve/merge if all is fine.
I think after merging this we should add some negative tests too.

chriseth · 2023-05-24T11:39:35Z

halo2/src/mock_prover.rs

+            panic!();
+        });
+
+        let query_callback = |query: &str| -> Option<Bn254Field> {


It would be nice to reduce code duplication here, especially since I'm changing the query format from time to time...

I'm also fine with moving this to witgen and have one "default" query callback that takes a vector of numbers, but also the option for the user to change it if they do custom pil.

Haha yes an outdated query format made me waste an hour when working on this PR. I think having a default one makes sense. I opened #302 for it.

leonardoalt force-pushed the halo_poc branch from 7598915 to 0a239fa Compare April 6, 2023 15:54