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

Initial draft for `move-sui`'s `Bytecode` type #576

Closed InfiniteEchoes closed 4 months ago

InfiniteEchoes commented 4 months ago

Add initial draft to start the project, since Bytecode type is almost required by every other files.