verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src modes.md
1.5 kB · 37 lines
Markdown
at master

Specification code, proof code, executable code #

Verus classifies code into three modes: spec, proof, and exec, where:

  • spec code describes properties about programs
  • proof code proves that programs satisfy properties
  • exec code is ordinary Rust code that can be compiled and run

Both spec code and proof code are forms of ghost code, so we can organize the three modes in a hierarchy:

  • code
    • ghost code
      • spec code
      • proof code
    • exec code

Every function in Verus is either a spec function, a proof function, or an exec function:

{{#include ../../../../examples/guide/modes.rs:fun_modes}}

exec is the default function annotation, so it is usually omitted:

{{#include ../../../../examples/guide/modes.rs:fun_modes2}}

The rest of this chapter will discuss these three modes in more detail. As you read, you can keep in mind the following relationships between the three modes:

spec code proof code exec code
can contain spec code, call spec functions yes yes yes
can contain proof code, call proof functions no yes yes
can contain exec code, call exec functions no no yes