[fix] soundness bug in BasicDynLookupConfig::assign_virtual_table_to_raw
#224
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The problem is that in
assign_virtual_table_to_raw
it was usingassign_virtual_to_raw
, which has the following danger:HashMap
ofassigned_advices
. However later theBaseCircuitBuilder
raw_assign
might overwrite this assignment without adding any real equality constraints. Therefore the first raw cell becomes a dangling unconstrained cell.The fix is that now
assign_virtual_table_to_raw
usesconstrain_virtual_equals_external
, and we have modifiedconstrain_virtual_equals_external
so that it checks whether the virtual cell has already been assigned or not. It is only allowed to not have been assigned if thetype_id
of the virtual cell was marked asEXTERNAL_CELL_TYPE_ID
. This marks the virtual cell as safe from ever being reassigned by a different virtual region manager.EXTERNAL_CELL_TYPE_ID
, then we assign the virtual cell to the new external cell.The usage in the latter case is demonstrated in the
memory.rs
test.We add a check whenever we do
assigned_advice.insert
that there was not already a cell present or that the occupied raw cell equals the raw cell to be inserted (this latter case is just becausekeygen_vk
andkeygen_pk
each callsynthesize
and we cannot callclear
because of mutable borrows).