Here's the initial version of quint stubs generation for cosmwasm contracts. This version works for ctf01 and ctf02.
I'm using the rustc_plugin crate to define a compiler callback that prints quint to STDOUT. The core is implemented over the rustc_hir (Rust's High-Level IR), so we can freely change how the tool is called, as long as it receives the HIR for the CosmWasm project.
File structure
lib.rs - Main file, which iterates over items of the HIR calling the translate function
translate.rs - Translation trait and its implementation for all necessary HIR nodes (plus a few intermediate representation types I had to add, like Field and Function)
types.rs - Auxiliary type definition, mainly Context. Context became quite polluted, I'll try to improve that over time.
boilerplate.rs - Big strings to be printed for making the quint module complete
nondet.rs - How we translate values to be given for things in the actions
state_extraction.rs - Hacky way to extract state variables out of rust constants.
HIR Navigation
This is recursing into the HIR via the Translatable trait translate functions. These functions take a context and return a string, therefore, any information that needs to be passed beteween different components should be added to the context.
The context is mutable for now, as this seems to be the rust way. We might want to make it non-mutable if the mutability gets too confusing. I'm already having to "remember" to clear data from the context after consuming it in some places.
Hello :octocat:
Here's the initial version of quint stubs generation for cosmwasm contracts. This version works for ctf01 and ctf02.
I'm using the rustc_plugin crate to define a compiler callback that prints quint to STDOUT. The core is implemented over the
rustc_hir(Rust's High-Level IR), so we can freely change how the tool is called, as long as it receives the HIR for the CosmWasm project.File structure
lib.rs- Main file, which iterates over items of the HIR calling thetranslatefunctiontranslate.rs- Translation trait and its implementation for all necessary HIR nodes (plus a few intermediate representation types I had to add, likeFieldandFunction)types.rs- Auxiliary type definition, mainlyContext.Contextbecame quite polluted, I'll try to improve that over time.boilerplate.rs- Big strings to be printed for making the quint module completenondet.rs- How we translate values to be given for things in the actionsstate_extraction.rs- Hacky way to extract state variables out of rust constants.HIR Navigation
This is recursing into the HIR via the
Translatabletraittranslatefunctions. These functions take a context and return a string, therefore, any information that needs to be passed beteween different components should be added to the context.The context is mutable for now, as this seems to be the rust way. We might want to make it non-mutable if the mutability gets too confusing. I'm already having to "remember" to clear data from the context after consuming it in some places.