Complete implementation for Verify
#744
Conversation
|
@ia0 Could you also take a look at the follow-up PR in my fork? Thanks. |
| @@ -132,13 +132,18 @@ impl<'m> BranchTableApi<'m> for &mut Vec<BranchTableEntry> { | |||
| } | |||
| } | |||
|
|
|||
| struct MetadataView<'m> { | |||
There was a problem hiding this comment.
This is good to have side table views specific to verification in valid.rs because exec.rs will need different views (it won't need the mutable index used only for verification).
| fn stitch_branch( | ||
| &mut self, source: SideTableBranch<'m>, target: SideTableBranch<'m>, | ||
| ) -> CheckResult { | ||
| check(source == target) | ||
| } | ||
|
|
||
| fn patch_branch(&self, mut source: SideTableBranch<'m>) -> Result<SideTableBranch<'m>, Error> { | ||
| let entry = self.branch_table()[source.branch_table].view(); | ||
| source.branch_table = self.branch_idx; |
There was a problem hiding this comment.
I'm a bit surprised by this. In theory, we should have source.branch_table + 1 == self.branch_idx, so this smells like an off-by-one error. Let's merge like this but keep it in mind. This might be a source of error.
There was a problem hiding this comment.
Could you explain why you believe so?
Before this function, next_index() and allocate_branch() are called.
For Prepare, next_index() returns the length of the branch table, and allocate_branch() pushes an invalid entry to the branch table, which patch_branch returns.
For Verify, to be consistent with Prepare, I thought we should also use the next branch in patch_branch().
There was a problem hiding this comment.
For
Verify, to be consistent withPrepare, I thought we should also use the next branch inpatch_branch().
What does this mean?
patch_branch() should only do something in Verify (which is why it's the identity function in Prepare). In Verify it is supposed to convert the source branch to its target branch using the branch table. The branch index is given by the source branch. We shouldn't access branch_idx at all in this function. This field is only meaningful for next_index() and allocated_branch(), because it represents the current length of the branch table. In practice, patch_branch() is called right after the source branch is created, so it's the current last branch (thus its index is one less than the current length), but we shouldn't rely on this, in particular because it doesn't bring anything.
#46