ckb-vm icon indicating copy to clipboard operation
ckb-vm copied to clipboard

Formally Verify CKB-VM via Sail

Open xxuejie opened this issue 3 years ago • 0 comments

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

xxuejie avatar Aug 05 '21 07:08 xxuejie