Compiled should introduce an optimalisation and inject helper unconstrained functions to help with division.

[LogvinovLeon]

Problem

This section of docs describes the optimalization that if some computation is cheaper to verify than compute - we should compute it in unconstrained code and only verify the results in constrained.

In general case - this is too high level for an optimiser to pick up.
For integer division - it can be done quite easily and introduce measurable benefits.

Happy Case

When compiler see integer division - it should replace it with an unconstrained division and constrained multiplication reducing the backend circuit size

Alternatives Considered

No response

Additional Context

I've recently submitted a PR to noir-trie-proofs that does this optimalisation manually and it saves 3% of gates.
aragonzkresearch/noir-trie-proofs#11

Would you like to submit a PR for this Issue?

Maybe

Support Needs

I might be interested in submitting a PR with this change, but I'll need some guidance. Please let me know if you think it's a good idea and where would be the best stage to do a transformation like that.

[TomAFrench]

All division is unconstrained division! Whenever we do integer division we calculate the quotient and remainder in an unconstrained function, range constrain these two witnesses, and then enforce that numerator = quotient * denominator + remainder.

noir/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

Lines 714 to 762 in 26e9618

	let [q_value, r_value]: [AcirValue; 2] = self
	.brillig(
	predicate,
	brillig_directive::directive_quotient(bit_size + 1),
	vec![
	AcirValue::Var(lhs, AcirType::unsigned(bit_size)),
	AcirValue::Var(rhs, AcirType::unsigned(bit_size)),
	],
	vec![AcirType::unsigned(max_q_bits), AcirType::unsigned(max_rhs_bits)],
	true,
	)?
	.try_into()
	.expect("quotient only returns two values");
	let quotient_var = q_value.into_var()?;
	let remainder_var = r_value.into_var()?;
	// Constrain `q < 2^{max_q_bits}`.
	self.range_constrain_var(
	quotient_var,
	&NumericType::Unsigned { bit_size: max_q_bits },
	None,
	)?;
	// Constrain `r < 2^{max_rhs_bits}`.
	//
	// If `rhs` is a power of 2, then is just a looser version of the following bound constraint.
	// In the case where `rhs` isn't a power of 2 then this range constraint is required
	// as the bound constraint creates a new witness.
	// This opcode will be optimized out if it is redundant so we always add it for safety.
	self.range_constrain_var(
	remainder_var,
	&NumericType::Unsigned { bit_size: max_rhs_bits },
	None,
	)?;
	// Constrain `r < rhs`.
	self.bound_constraint_with_offset(remainder_var, rhs, predicate, max_rhs_bits)?;
	// a * predicate == (b * q + r) * predicate
	// => predicate * (a - b * q - r) == 0
	// When the predicate is 0, the equation always passes.
	// When the predicate is 1, the euclidean division needs to be
	// true.
	let rhs_constraint = self.mul_var(rhs, quotient_var)?;
	let rhs_constraint = self.add_var(rhs_constraint, remainder_var)?;
	let rhs_constraint = self.mul_var(rhs_constraint, predicate)?;
	let lhs_constraint = self.mul_var(lhs, predicate)?;
	self.assert_eq_var(lhs_constraint, rhs_constraint, None)?;

A lot of the savings that from that refactor come down to:

• The bug which is being fixed in fix: apply range constraints to return values from unconstrained functions #4217 (something I noticed due to this issue so thank you!)
• No longer doing bitwise ANDs (these are really unnecessary as it's equivalent to taking the remainder from a division in this case, something we're doing when casting to a u4 anyway)
• Using the results from a single euclidean division to give both nibbles in a byte rather than doing a euclidean division for each nibble.

The last one is a potential compiler improvement but it would require us to cache a lot of division results and the situations where it would come up most (splitting an integer into limbs of smaller integers) are easy enough to recognise that I think that adding a fn split_byte(byte: u8) -> (u4, u4) with an unconstrained helper would handle most cases.