lets-prove-leftpad icon indicating copy to clipboard operation
lets-prove-leftpad copied to clipboard

Published 20 hours ago • verified publisher icon hwayne

Rust example

Open suhr opened this issue 1 year ago • 3 comments

I proved leftpad in rust, using creusot: https://github.com/suhr/leftpad

How to verify:

  • cargo creusot --span-mode=absolute -- --features=contracts
  • «creusot repo»/ide target/debug/leftpad-rlib.mlcfg

NB: you need to apply “Split VC” on the leftpad VC to avoid CVC5 timeout.

Creusot is a research software, so I'm not sure if I should make a PR yet.

suhr avatar Jul 16 '22 19:07 suhr

Oooh! I tried with MIRAI in #43 and couldn’t get it to do even very simple things; I’m glad there’s another Rust solution now.

dhouck avatar Jul 17 '22 03:07 dhouck

Known experience, a year ago I tried to prove leftpad using prusti, with no success. Creusot seems to be the first actually usable tool for deductive verification in rust.

suhr avatar Jul 17 '22 07:07 suhr

Make the PR!

hwayne avatar Jul 17 '22 18:07 hwayne