formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
GNU Affero General Public License v3.0
418 stars 14 forks source link

Various updates of monads and lenses for simulations #579

Closed olympichek closed 4 months ago

olympichek commented 4 months ago

This pull request implements various updates of monads and lenses for simulations:

Additionally, REVM stack operations are rewritten using LensPanic. This provides an example of how lenses can be used to represent subpointers (mutable references). In this example, LensPanic is necessary, as the lens is used to represent top_unsafe operation, which fails with a panic when called on an empty stack.

InfiniteEchoes commented 4 months ago

Is it that the Result and Option monads are corresponded exactly to the Result & Option type in Rust?

olympichek commented 4 months ago

Is it that the Result and Option monads are corresponded exactly to the Result & Option type in Rust?

Yes, that's the idea