lambda-rust integration

[sethahrenbach]

I've been looking at the lambda-rust and Iris libraries as a way to verify properties about non-smart-contract Rust code. How heavy of a lift do you think it would be for me to make use of your libraries, integrating lambda-rust or Iris in place of lambda-smart?

[spitters]

We are currently making the last printing step to surface rust. lambda-rust is a model for MIR, so one could try to emulate/verify the step from from surface rust to MIR.
We are also working on a project to generate wasm directly using the certicoq pipeline, one could generate rust instead.
Finally, we are working on embedding "functional rust" (hacspec-v2).

Does any of that fit your use case?

[spitters]

We defined lambda-smart on p5 here. It's not restricted to smart contract languages. It would be a good target for the "functional"/linear part of rust, as defined in the hacspec language.
A more general embedding of rust into Coq is planned with https://github.com/AeneasVerif/aeneas
Its functional subset should agree with hacspec, at least in spirit.

[sethahrenbach]

Ok, I think for my initial use case I can examine how you are modeling, verifying, and extracting the even test. Thank you for the additional paths to explore, I'll be back.

[sethahrenbach]

Oh, additionally, I'm trying to step through the .v files in VS Code with the coq ide extension, but for your project files it cannot find the path. E.g. Cannot find a physical path bound to logical path Loader with prefix ConCert.Extraction.coqtop from file ConCert/extraction/plugin/theories/InternalFix.v

[4ever2]

If you are using the VSCoq extension then you need to set the correct path to the _CoqProject file. In ConCert we have different _CoqProject files for each subpart of the project. For the specific file you are trying to step through you need to add "coq.coqProjectRoot" : "./extraction/plugin/" to your workspace settings.