-
Notifications
You must be signed in to change notification settings - Fork 43
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
IgnoreMaxNS leads to false computing maxNs #148
Comments
Here is the link to the issue on the audit repo. |
Resolution of this issue should be aligned with the rephrased comment in Reworded explanation of calculating namespace when IgnoreMaxNamespace is set. |
…ered ascendingly (#188) ## Overview Closes #121 and #148. Please refer to this [PR](#193) to compare the new and old version of namsespacre range calculation for a parent node in the `HashNode()`. ## Checklist - [x] New and updated code has appropriate documentation - [x] New and updated code has new and/or updated testing - [x] Required CI checks are passing - [x] Visual proof for any user facing features like CLI or documentation updates - [x] Linked issues closed with keywords
This issue has been resolved through the following pull request: link. The PR incorporates specific unit tests that focus on the calculation of namespace ranges for nodes. These calculations are based on the namespaces of their respective left and right children, specifically when the IgnoreMaxNamespace flag is enabled. These additions to the codebase aim to provide a clear understanding of the expected behavior when this flag is turned on. |
<!-- Please read and fill out this form before submitting your PR. Please make sure you have reviewed our contributors guide before submitting your first PR. --> ## Overview This PR introduces a formal specification of the NMT proof/verification logic in [Quint](https://github.com/informalsystems/quint). The benefits of having a Quint specification are threefold: - It is a precise description of the expected behavior, and yet it resides on a higher level of abstraction than the code. Furthermore, it is executable, which makes it easier to spot and eliminate mistakes in the specification. Module [nmt](https://github.com/ivan-gavran/nmt/blob/c3cc6b7acba34c97a1a4d5e8fa4be1d355535c1e/formal_spec/nmt.qnt#L253) captures the logic of namespace proof generation and verification, and the invariant [`verificationAlwaysCorrect`](https://github.com/ivan-gavran/nmt/blob/c3cc6b7acba34c97a1a4d5e8fa4be1d355535c1e/formal_spec/nmt.qnt#L592) is an example of a property against which a specification can be checked. - It allows for test generation. Module [`nmtTest`](https://github.com/ivan-gavran/nmt/blob/c3cc6b7acba34c97a1a4d5e8fa4be1d355535c1e/formal_spec/nmt.qnt#LL597C17-L597C17) iteratively generates proofs and non-deterministically corrupts them. These generated test runs are exported in a json format (e.g., file [ITF_traces/runTest.itf.json](https://github.com/ivan-gavran/nmt/blob/ivan/quint_spec/formal_spec/ITF_files/runTest.itf.json)). To be executed as a part of the standard suite, an adapter [simulation_test.go](https://github.com/ivan-gavran/nmt/blob/ivan/quint_spec/simulation_test.go) is necessary. (The adapter iterates through the json-represented execution state and translates them to function calls.) The generation of the tests happens through simulation. In that sense, it is similar to the existing tests [fuzz_test.go](https://github.com/celestiaorg/nmt/blob/master/fuzz_test.go), except that it also adds corruption of the data. - Having specifications written in Quint makes it possible to change tests/specs quickly: either by taking advantage of updates to Quint (e.g., going from simulation to exhaustive checks by changing a command) or by virtue of making changes on the level higher than code (and thus less details need to be changed). Current limitations: - the specification does not model absence proofs - there is an assumption that every tree is full and complete - the specification does not model special handling of parity namespace (`ignoreMaxNamespace` option). Modelling it correctly depends on the decision of what the desired behaviour is (issue #148 ) ## Checklist <!-- Please complete the checklist to ensure that the PR is ready to be reviewed. IMPORTANT: PRs should be left in Draft until the below checklist is completed. --> - [ ] New and updated code has appropriate documentation - [ ] New and updated code has new and/or updated testing - [ ] Required CI checks are passing - [ ] Visual proof for any user facing features like CLI or documentation updates - [ ] Linked issues closed with keywords
I am moving the issues from our audit collaboration repo to the nmt repo, because we decided to report issues here. It would be easier to follow the progress.
Here is the description of the issue about computing
maxNs
withn.ignoreMaxNS
set to true that we discussed about.We are not sure what is the expected behavior when it comes to calculating
maxNs
withn.ignoreMaxNS
set to true.As we understand the expected behavior under these conditions is to choose a
maxNs
that is less thann.precomputedMaxNs
if possible. If this is the case there might be an issue with computingmaxNs
here, which can lead to setting it ton.precomputedMaxNs
even if it could be set to a namespaceId that is smaller thann.precomputedMaxNs
.If we assume the following:
n.ignoreMaxNS = true
leftMinNs != n.precomputedMaxNs
rightMaxNs = n.precomputedMaxNs
rightMinNs < n.precomputedMaxNs
rightMinNs>leftMaxNs
.Than the
maxNs
will be set ton.precomputedMaxNs
even if it should be set torightMinNs
because it is the largest namespaceId smaller thann.precomputedMaxNs
.Example with numbers (presented also in the image at the end):
Lets assume that following:
Based on this logic in
HashNode
theminNs
and `maxNs' for the node that is being calculated will take the following values:precomputedMaxNs
(because theelse
branch of the if statement will be executed and there 10 will obviously be chosen even if theright.minNs
is larger thenleft.maxNs
but not equal toprecomputedMaxNs
).This numerical example with the current behavior and the behavior we expect is graphically presented in the following image.
The text was updated successfully, but these errors were encountered: