zcash / halo2

The Halo2 zero-knowledge proving system
https://zcash.github.io/halo2/
Other
733 stars 496 forks source link

Add support for `Value::one()` and `Value::zero()` and maybe, `Value::<F::From>::from()` #698

Open CPerezz opened 1 year ago

CPerezz commented 1 year ago

It's just quite annoying the need to express Value::known(F::one()) when it's implicit that if you're passing one, the value is known. Same happens with 0.

And this verbosity is extending significantly across the entire zkevm-circuits repo for example. Where we have +100 places where this happens for 1 or 0. Also, there's +150 places where Value::known(F::from(x)) appears. This just feels the same for me, as if you pass a value to construct a Value, it definitely has to be known and therefore, the call to known can be implicit.

Is this something you do also experience on Orchad circuits? Have you ever been thought about this too/would consider to adopt it??

daira commented 1 year ago

Yes we have quite a few instances of Value::known constructors for the constants 1 (7 cases), 0 (11 cases), and -1 (14 cases) in the Orchard circuit. We also have 6 conversions from other 64-bit constants using Value::known(pallas::Base::from(...)), and 26 conversions from other 128-bit constants using Value::known(pallas::Base::from_128(...)).

These are all in src/circuit/note_commit.rs and src/circuit/commit_ivk.rs.

CPerezz commented 1 year ago

I'll try to work on this and see if I can come up with something that reduces a bit the overhead.

Thanks for the data @daira ! I was afraid we were doing something really wrong lol

str4d commented 1 year ago

The tricky part with providing these is that there exist no standard library traits for Zero or One, so we can't provide blanket impls of Value::zero or Value::one without inherently limiting the types that it can apply to. For example, we could have a blanket impl for these on all types F: Field (which would solve your issue), but then we can't do the same for Value<u64> etc. (because the traits would overlap). We could try and define our own traits for these, but things start getting trickier if these traits are "above" the types they apply to. So this will need some experimentation.

str4d commented 1 year ago

This does not work:

pub trait ValueExt {
    const ZERO: Self;
    const ONE: Self;
}

impl ValueExt for Value<u64> {
    const ZERO: Value<u64> = Value::known(0);
    const ONE: Value<u64> = Value::known(1);
}

impl<F: Field> ValueExt for Value<F> {
    const ZERO: Value<F> = Value::known(F::ZERO);
    const ONE: Value<F> = Value::known(F::ONE);
}

for the reason I described above:

error[E0119]: conflicting implementations of trait `circuit::value::ValueExt` for type `circuit::value::Value<u64>`
  --> halo2_proofs/src/circuit/value.rs:60:1
   |
55 | impl ValueExt for Value<u64> {
   | ---------------------------- first implementation here
...
60 | impl<F: Field> ValueExt for Value<F> {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `circuit::value::Value<u64>`
   |
   = note: upstream crates may add a new impl of trait `ff::Field` for type `u64` in future versions

For more information about this error, try `rustc --explain E0119`.

However, if we are content to have separate extension traits for primitive types and F: Field types, then we can do something like it, which I've implemented in #699 for testing purposes.

CPerezz commented 1 year ago

Extending the discussion in https://github.com/zcash/halo2/pull/699 about traitifying Value<T> or any other ideas.

str4d commented 1 year ago

Bringing the general discussion back in here.

@CPerezz said in https://github.com/zcash/halo2/pull/699#issuecomment-1334277281:

For some reason I was thinking that maybe GATs would allow us to do something like:

pub trait Value<T> {
    type Inner: Option<T>;
}

EDIT: It's Associated Type Defaults what would solve the issue of constraining more the inner type.

Then we can define the same exact implementations for Value generically and add a few extra if needed. I understand this would bring issues anyway as then it's up to the implementor to implement Value on a correct way. But at least was giving a lot of expressiveness. And you are also "enforcing the implementor" to consider the inner item of Value as something that might be unknown or None etc...

For Associated Type Defaults to help here, we'd need a separate trait that is a bound on Inner above, which enforces the maybe-known-ness of a value (because Inner: Option<T> does not work, and type Inner = Option<T> removes entirely any enforcement on the implementor, and in fact prevents the halo2 backend from being able to distinguish the two cases entirely). While I'm sure it's theoretically possible to implement an enum in the type system, I'm not convinced that it would be at all ergonomic. But I'd be happy to be proven wrong!

In any case, the reason why the concrete type Value<V> was introduced is that Option<V> has Option::unwrap which was a huge footgun for circuit developers (resulting in both circuit bugs and unsound circuits IIRC). Your above suggestion feels more to me like:

pub trait SomeValueWrapper<V> {
    type Inner = Value<T>;
}

where (ignoring the ATD issue I outlined above) we have the core inner type being a "value in a circuit cell", and a generic ergonomic wrapper around it. But then that is what we are already trying to provide with the concrete Value<V> type, extending its API with traits.

I think anyway, that right now, Value is really tied to Field/FieldExt struct implementors. But if we traitify it, we could extend it to elliptic curve points for example or other stuff.

Value isn't tied to Field AFAICT; every method on Value<V> has either no bounds on V, or bounds using traits from the standard library (e.g. Add or FromIterator). There are Field-specific methods for Value<Assigned<F: Field>>, but that is because Assigned<F> has an F: Field bound; it isn't because of Value.

What are the problems you are running into using Value<EllipticCurvePoint> (or Value<u64 etc)?

There are times where we need to decompose a Value into bytes. And it's simply a nightmare. When instead we could have a From implementation or some similar thing that returned the [Value<F>; 32]. Same thing for bit representations. That also happens for some XOR/Bitwise ops etc... SHR, SHL....

The core issue here is that there is no common trait for "decompose into bytes" (partly because const generics aren't advanced enough, but also I suspect because this abstraction is too abstract). Instead you have either context-specific generic traits like ff::PrimeField / group::GroupEncoding, or concrete methods on V that we can't access in a generic context.

For this particular example, I presume that what you are describing looks something like this (please give a more concrete example if this one is incorrect):

let foo: Value<jubjub::ExtendedPoint> = ...; // from somewhere
let bar: Value<[u8; 32]> = foo.map(|p| p.to_bytes());
let baz: [Value<u8>; 32] = bar.transpose_array();

or more concisely (which is what you'd actually write; the above is just to show the types):

let foo = ...; // A Value<jubjub::ExtendedPoint> from somewhere
let baz = foo.map(|p| p.to_bytes()).transpose_array();

This seems fine to me? It's about as concise as I can imagine this being for the logically-equivalent fn(Option<jubjub::ExtendedPoint>) -> [Option<u8>; 32] - in fact, it's more concise because we provide Value::transpose_array.

It feels to me like some of the current issues can be addressed with more standard library trait helpers. The above works because we have [V; const LEN: usize] generics, and there's nothing preventing us from adding similar convenience impls like impl<V: Shl> Shl for Value<V> (it's just that no one has requested them yet).

CPerezz commented 1 year ago

Thanks for the elaborated reply @str4d .

The transposing example is brilliant. And I did not think about it. Considering that this solves byte-conversion, we lack the one, zero and From<u8, u16,....u128>. We also lack from_bytes() and finally shifting ops. (At least these are all the cases we use at PSE). I agree that the From is not a real issue. Just verbosity. But the from_bytes or the shifting causes us to "cheat" to the API by mapping a Value and assigning the internal field to a mut field declared outside to gain access to the F.

I'll try to submit a PR with the things that would be required for us. And see if we can avoid bigger refactors which do not clearly bring an improvement to the current API.