Verify PeerList with Stainless

[yannbolliger]

This is a first trial to introduce cargo stainless and let it run on the PeerList.

Problems that came up:

• No support for constants Support constants epfl-lara/rust-stainless#73
• No type aliases Extract type aliases epfl-lara/rust-stainless#141
• contracts crate has a ==> macro feature for implies in specs. (won't fix)
• Stainless collections don't have the same names as Rust's std ones. Examples: Stainless Map has contains instead of contains_key, the Set has add instead of insert. Stainless collection method names epfl-lara/rust-stainless#144
• No mutable references/borrowing, this was easily circumvented by locally mutating and consuming the self: 858da86. Spec macro fails on mut self param epfl-lara/rust-stainless#145
• External files with modules of the same crate work. But, the mod xx; use xx::*; and the corresponding use super::*; fail as unsupported trees. Allow imports (use) statements epfl-lara/rust-stainless#146
• Sometimes, Stainless complains that it can't extract the tree kind lifetime. Could these just be ignored? Example: pub fn first(&self) -> Option<&T> { ... }. Ignore Lifetimes epfl-lara/rust-stainless#147
• No higher-order functions for things like iter().all(...). This was easily circumvented by creating some new set methods.
• The trait bounds that are now required on stainless::{Set, Map}, namely T: Eq + Hash + Clone, force users that also implement something generic (for example the ListSet) to put the same trait bounds on their implementation. These bounds then create evidence arguments everywhere that are for types that are not extracted. Hence, Stainless fails with missing dependencies. Unfortunately, this makes the new runtime implementations for stainless::{Set, Map} quite unusable.
  • One idea was to conditionally (on --cfg stainless) compile with the trait bounds for the runtime version and without them for cargo stainless. This fails due to the one-crate-only compilation model. The stainless::{Set, Map} are outside of the current crate. Could a prelude be the solution to this?
  • Another idea would be to ignore/erase all the three traits Eq + Hash + Clone and their corresponding evidence args.
  • The final idea is Extract external trait signature for bounds/evidence args epfl-lara/rust-stainless#143

Findings (Tendermint-related)

• The postconditions on the two methods replace_faulty_witness, replace_faulty_primary only hold if the precondition includes/validates the invariant. Should this be added / was that implicitly assumed?

---

• Referenced an issue explaining the need for the change
• Updated all relevant documentation in docs
• Updated all code comments where relevant
• Wrote tests
• Updated CHANGELOG.md

[romac]

The postconditions on the two methods replace_faulty_witness, replace_faulty_primary only hold if the precondition includes/validates the invariant. Should this be added / was that implicitly assumed?

Good catch, feel free to open a PR to fix this, and make sure to mention there how you figured this out :)

[codecov-commenter]

Codecov Report

Merging #866 (75440f9) into master (d8e18c6) will decrease coverage by 0.0%.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           master    #866     +/-   ##
========================================
- Coverage    70.6%   70.5%   -0.1%     
========================================
  Files         203     203             
  Lines       16303   16343     +40     
========================================
+ Hits        11515   11527     +12     
- Misses       4788    4816     +28     

Impacted Files	Coverage Δ
rpc/src/endpoint/validators.rs	9.0% <0.0%> (-41.0%)	⬇️
abci/src/server.rs	9.8% <0.0%> (-0.8%)	⬇️
tendermint/src/node.rs	65.9% <0.0%> (-0.3%)	⬇️
light-client/src/types.rs	30.9% <0.0%> (+0.5%)	⬆️
tendermint/src/config.rs	65.7% <0.0%> (+1.3%)	⬆️
tendermint/src/signature.rs	62.5% <0.0%> (+3.5%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d8e18c6...75440f9. Read the comment docs.

[thanethomson]

Is this PR still relevant in any way?