Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor for basic constraints #48

Closed
wants to merge 27 commits into from

Conversation

katat
Copy link
Collaborator

@katat katat commented Apr 22, 2024

  • add basic constraint interfaces to the backend: neg / add / mul / assert_eq
  • refactor boolean constraints
  • refactor field constraints
  • refactor builtin constraints
  • move some logic from add_public_outputs and add_public_inputs to the backend (to remove the add_gate stuff)

Copy link
Contributor

@mimoo mimoo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is going in the right direction! Obviously this is going to make our constraints less efficient, but we can fix this in a later PR

lhs: &ConstOrCell<Self::Field>,
rhs: &ConstOrCell<Self::Field>,
span: Span,
) -> ConstOrCell<Self::Field>;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would call these neg, add, and mul as they might not create a constraint eventually.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

also as I hint later, I think they should not receive ConstOrCell but CellVar instead

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It now uses CellVar at the backend layer

),
ConstOrCell::Cell(_) => {
// x * (x - 1)
let x_1 = field::sub(compiler, xx, &ConstOrCell::Const(one.neg()), span);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

one not one.neg()

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fixed

);
let res_mul_diff = mul(compiler, &ConstOrCell::Cell(res), &diff, span)[0];
// ensure that res * diff = 0
sub(compiler, &res_mul_diff, &ConstOrCell::Const(zero), span);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is a no-op, instead what we want to do here is assert_eq(res_mul_diff, zero), where assert_eq is also exposed by the backend

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it is now enforced by assert_eq

span,
);
let diff_inv_mul_diff = mul(compiler, &ConstOrCell::Cell(diff_inv), &diff, span)[0];
sub(compiler, &diff_inv_mul_diff, &one_minus_res, span);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here, either assert_eq(diff_inv_mul_diff, one_minus_res) or assert that the result of sub is equal to zero.

BTW we also should add #[must_use] to these functions (sub, neg, etc.) as well as trait functions (the one you added to do sub, neg, mul, etc.) so that the compiler yells at us if we don't use a var or a cvar from an operation


match (lhs, rhs) {
// 2 constants
(ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs + *rhs, span),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so my feeling is that it would be more elegant to leave the code handling constants here. Perhaps this means that in the backend we would also have: add_const(const: F, cvar: CellVar<F>) and scale(coeff: F, cvar: CellVar<F>)

this way the handling of pure constants is not done in the backend

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this one should be fixed

examples/arithmetic.no Outdated Show resolved Hide resolved
@katat katat force-pushed the refactor/basic-constraints branch from 0c45057 to e4cd10f Compare April 23, 2024 08:45
@katat katat marked this pull request as ready for review April 23, 2024 08:54
Copy link
Contributor

@mimoo mimoo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

went through it quickly and left you a number of comments, but the main one will be the same as with the other PR :D can you create easy-to-review commits?

@@ -133,58 +136,11 @@ impl KimchiVesta {
pending_generic_gate: None,
debug_info: vec![],
finalized: false,
public_input_size: 0,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

would it make sense to pass that as argument in new()?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

actually it doesn't make sense, rereading things, as it gets calculated when we call add_public_input and add_public_output

Copy link
Collaborator Author

@katat katat Apr 26, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yeah, I was wondering this fact also

@@ -546,4 +551,159 @@ impl Backend for KimchiVesta {

res
}

fn constraint_neg(&mut self, var: &CellVar, span: Span) -> CellVar {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

remove constraint from the name (so just neg) as it wrongly imply that we will create a constraint here (same for others)

fn constraint_eq_const(&mut self, var: &CellVar, cst: Self::Field, span: Span);

/// add a constraint to assert a var equals another var
fn constraint_eq_var(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

none of these functions have to add a constraint, so constraint should be removed from the name and the doc

@mimoo mimoo closed this Apr 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants