Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
<!-- 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
- Loading branch information
1 parent
6854976
commit 033ce9e