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

Formally Verify CKB-VM via Sail #190

Open
xxuejie opened this issue Aug 5, 2021 · 0 comments
Open

Formally Verify CKB-VM via Sail #190

xxuejie opened this issue Aug 5, 2021 · 0 comments

Comments

@xxuejie
Copy link
Collaborator

xxuejie commented Aug 5, 2021

Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. The formal specification of RISC-V ISA is defined exactly in sail.

We could leverage sail to compile x86 and RISC-V models both down to Coq definitions. From there we can formally prove that our x86 assembly implementation of each RISC-V instruction, fully confronts to the RISC-V official specification.

Later when an aarch64 implementation is introduced, we could leverage the same proving techniques here.

This solution has the issue that Rust based interpreter cannot be proved. But once we have a formally proved assembly based fast implementation, not so many will care about Rust based interpreter :P

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant