Skip to content

Use closures in enforce_constraints#405

Merged
Pratyush merged 8 commits into
masterfrom
use-closures-for-constraints
Jun 12, 2025
Merged

Use closures in enforce_constraints#405
Pratyush merged 8 commits into
masterfrom
use-closures-for-constraints

Conversation

@Pratyush

Copy link
Copy Markdown
Member

Description

closes: #XXXX


Before we can merge this PR, please make sure that all the following items have been
checked off. If any of the checklist items are not applicable, please leave them but
write a little note why.

  • Targeted PR against correct branch (master)
  • Linked to Github issue with discussion and accepted design OR have an explanation in the PR that describes this work.
  • Wrote unit tests
  • Updated relevant documentation in the code
  • Added a relevant changelog entry to the Pending section in CHANGELOG.md
  • Re-reviewed Files changed in the Github PR explorer

},
cache_map: Rc::new(RefCell::new(BTreeMap::new())),
lc_map: Vec::new(),
lc_map: vec![Some(LinearCombination::zero())],

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

We add an empty LinearCombination into the map, so that constraints which use empty linear combinations (e.g. via lc!()) can refer to this specific LC instead of always spawning a new one.

Comment on lines +287 to +291
let lc = lc();
match lc.0.as_slice() {
// If the linear combination is empty, we return a symbolic LC with index 0.
// If the linear combination is just Zero, we return a symbolic LC with index 0.
[] | [(_, Variable::Zero)] => Variable::SymbolicLc(LcIndex(0)),

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

If the lc is empty or consists of a single element with Variable::Zero, then we return the index for the zero LC.

Comment on lines +294 to +305
[(c, var)] if c.is_one() => *var,
// In all other cases, we create a new linear combination
_ => {
let index = LcIndex(*num_lcs);
lc_map.push(Some(lc));
*num_lcs += 1;
if should_generate_lc_assignments {
let value = assignments.eval_lc(index, lc_map).unwrap();
assignments.lc_assignment.push(value)
}
Variable::SymbolicLc(index)
},

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

Otherwise, we create a new LC.

/// If the linear combination is already in the map, return the
/// corresponding index (using bimap)
/// Enforce a constraint for a predicate with arity 2.
pub fn enforce_constraint_arity_2(

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

We add helpers for specific arity constraints. This avoids the dyn object required by enforce_constraints

@Pratyush Pratyush requested review from Copilot and weikengchen June 11, 2025 05:29

This comment was marked as outdated.

Comment thread relations/src/utils/linear_combination.rs Outdated
Comment thread relations/src/utils/linear_combination.rs Outdated
Comment thread relations/src/utils/linear_combination.rs Outdated
Pratyush and others added 2 commits June 11, 2025 06:19
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Comment thread Cargo.toml Outdated
Comment thread relations/Cargo.toml Outdated
Comment thread relations/Cargo.toml Outdated
Comment thread relations/src/utils/linear_combination.rs Outdated
@Pratyush Pratyush requested a review from Copilot June 12, 2025 16:22

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Pull Request Overview

This PR updates constraint enforcement to use closures for constructing linear combinations, aiming for a more flexible and deferred evaluation of constraints. Key changes include:

  • Converting direct linear combination expressions into closures in various constraint enforcement functions.
  • Introducing a new lc_diff! macro and updating several tests, examples, and internal modules to follow the new API.
  • Refactoring parts of the constraint system to support closure evaluation for better modularity.

Reviewed Changes

Copilot reviewed 14 out of 14 changed files in this pull request and generated no comments.

Show a summary per file
File Description
relations/src/utils/linear_combination.rs Updated lc! macro and linear combination constructors to use closures.
relations/src/sr1cs/mod.rs Revised constraint enforcement to use closure syntax for operands.
relations/src/gr1cs/tests/* Updated tests to invoke constraint macros with closures.
relations/src/gr1cs/{predicate, constraint_system*, instance_outliner.rs} Refactored constraint API and internals to support closure-based evaluation.
relations/examples/* Updated examples to use closures when enforcing constraints.
relations/Cargo.toml Added mimalloc as a dependency.
Comments suppressed due to low confidence (2)

relations/src/gr1cs/constraint_system_ref.rs:238

  • When using closures for constraint enforcement, document that these closures must be pure and idempotent, as they might be invoked multiple times. Adding a comment or additional documentation here would help future maintainers avoid side-effect issues.
pub fn enforce_r1cs_constraint(&self, a: impl FnOnce() -> LinearCombination<F>, b: impl FnOnce() -> LinearCombination<F>, c: impl FnOnce() -> LinearCombination<F>) -> crate::gr1cs::Result<()> {

relations/src/gr1cs/constraint_system.rs:510

  • Consider adding inline comments or tests to clarify the handling of degenerate linear combinations (e.g., when the LC is empty or trivial) in new_lc_add_helper. This will ensure that the special-case logic remains clear and behaves as expected over time.
fn new_lc_add_helper( cur_num_lcs: &mut usize, lc_map: &mut Vec<Option<LinearCombination<F>>>, should_generate_lc_assignments: bool, assignments: &mut Assignments<F>, lc: LinearCombination<F>) -> crate::gr1cs::Result<Variable> {

@Pratyush Pratyush merged commit 9b991e0 into master Jun 12, 2025
4 checks passed
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.

3 participants