Fix the `outline_lcs`

[weikengchen]

After careful debugging, it appears that the current implementation of outline_lcs has two serious problems:

• It does not correctly create additional constraints. All the additional constraints should be LC * 1 = V where V is the new witness variable. In the end, all of them are V * 1 = V.

• It does not increase the count of num_linear_combinations correctly. So that in Marlin, when the next step wants to pad the matrices to be square, the new linear combinations go to the wrong linear combination entry, causing the outer check to fail.

This PR fixes these two problems and will close this issue in Marlin: https://github.com/arkworks-rs/marlin/issues/56

[weikengchen]

It turns out that I cannot assign a reviewer here. So, let me here cc Pratyush for a review. @Pratyush

We may, in the future, has an improvement plan for outline_lcs, since the resulting saving is not as large as expected.

[Pratyush]

Thanks for the PR! Given that there was a subtle bug in the logic here, would it be possible to add some comments documenting the algorithm?

[weikengchen]

No problem. On the way!

[weikengchen]

The documentation has been added. Please take a look :)

[weikengchen]

For the new_witness, yes, good point, let me use new_witness instead.

For the new constraint via enforce_constraint, it has a problem---our code is modifying the lc_map but enforce_constraint would also push to it, causing a conflict (that our code may overwrite the change). But let me take a more careful look to see I can still use enforce_constraint in a black-box way if I save the lc_map earlier.

[Pratyush]

For the new_constraint issue, maybe we can extract the common logic into a separate method that is called in both places?

[weikengchen]

Yes. But I feel that probably I can call new_constraint directly if I do self.lc_map = outlined_lcs; earlier, since these new constraints all use outlined LCs (so no more processing is needed).

[weikengchen]

I use new_constraint directly, so the code is now slightly simplified.

I didn't use new_witness for a specific reason:

• The new_witness somehow has to be in the for loop of self.lc_map. Moving it out could lead to potential missing assignments.
• But new_witness takes &mut self as input, but this is forbidden (since self is currently used for iteration).
• If I want to allow new_witness to use &mut self, I need to clone self.lc_map, but the memory usage might be too high.

Thus, given that the logic of new_witness is simple, I just write the same code again.

Note: I need to test the upstream Marlin for this PR to see if it is working. So don't merge now!

[Pratyush]

Hmm in that case we should document that this is the same logic as new_witness.

Also, speaking of memory requirements, we should "garbage-collect" the LCs that are inlined/put in new variables, like we do in inline_all_lcs

[weikengchen]

Got it. Let me have some tries.

[ValarDragon]

Thanks for fixing this bug!

[weikengchen]

More review is welcome. Let me merge the suggestions!

[weikengchen]

I updated the suggestions. Currently testing with Marlin.

@ValarDragon can do a final pass over the new comments that try to explain the loop.

[weikengchen]

The upstream test passes, and it is ready to merge if no other issues pop up.

[weikengchen]

(ps I need someone who has write access.)

[Pratyush]

Doing a final review pass, and then I'll merge!

[weikengchen]

Thanks for the review. I will resolve the comments soon and also merge the logic of the two functions for fewer repetitions.

(I might have some delays due to sending the Mac for fixing---my "e" key is now an "ee" key.)

[weikengchen]

Response to this:

In a future PR, I think we should be able to improve the efficiency by changing new_lc_map to being just a map of the differences (SymbolicLC -> Var). (Instead of making a copy of all the LC's)

Indeed almost all lcs would be rewritten due to inlining (all symbolic LCs are replaced by linear combinations of input/witness variables).

[weikengchen]

The implementation has been refactored in that the common elements between inline_all_lcs and outline_lcs are extracted.

@Pratyush @ValarDragon You may want to give a fresh reading to see if the logic flows right.

Note: The PR is not ready for merging, as I need to test it on Groth16 and Marlin.

[weikengchen]

And also, should we change outline_lcs to outline_all_lcs?

[weikengchen]

A bug has been fixed. It now passes on Groth16 and Marlin.

[weikengchen]

Opinions on changing outline_lcs to outline_all_lcs? This is a good chance to decide (since it has not been used anywhere else).

[Pratyush]

I think outline_lcs is better, as we're not outlining all the LCs, only those that are large, no?

[weikengchen]

That makes sense!

[ValarDragon]

This function is presumably not an external facing API right?

The external facing api should probably be "reduce_matrix_density"

[weikengchen]

Indeed it will be externally facing, in that Marlin calls outline_lcs instead of inline_all_lcs before converting the constraint system into a matrix.

Technically, outline_lcs is also mostly inlining.

[ValarDragon]

I see. I think we should make this function private, and make the external facing function reduce_matrix_arity (or reduce_constraint_density or something), which will then call this function. In the future, other matrix arity optimizations may make it in there.

[weikengchen]

I would call it reduce_constraint_weight since Ale uses weight in our paper on recursive Marlin.

[weikengchen]

Ok. The final change passes the CI.

I hereby need one person with write access to merge this PR.

[Pratyush]

In that case, should we provide a higher level API to inline_all_lcs too?

perhaps a single “finalize” method that takes in a rename OptimizationMode enum and then internally calls inline_lcs or outline_lcs? (This can be a separate PR)