Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Write simple simulations #511

Open
3 tasks
clarus opened this issue Apr 2, 2024 · 0 comments
Open
3 tasks

Write simple simulations #511

clarus opened this issue Apr 2, 2024 · 0 comments
Assignees

Comments

@clarus
Copy link
Collaborator

clarus commented Apr 2, 2024

Context: for now, we focus on the verification of the smart contracts, which are rather complex. We would like to have simpler examples to use as documentation/reference.

Write simulations, with their corresponding proof of equivalence, for a few simple examples that are already there in our Rust test suite. That could be simulations about examples handling the Option type, the Vec type, ...

  • write simulations for a few functions found in the translated Rust examples
  • show that these simulations are equal
  • add links to these examples in our Mardown documentation or even the README of the project
@clarus clarus moved this to Backlog in coq-of-rust Sprints Apr 2, 2024
@clarus clarus moved this from Backlog to Ready in coq-of-rust Sprints Apr 3, 2024
@InfiniteEchoes InfiniteEchoes self-assigned this Apr 6, 2024
@clarus clarus moved this from Ready to In progress in coq-of-rust Sprints Apr 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Status: In progress
Development

No branches or pull requests

2 participants