Skip to content

Latest commit

 

History

History
200 lines (172 loc) · 10.6 KB

README.md

File metadata and controls

200 lines (172 loc) · 10.6 KB
Raw

RustHornBelt COQ DEVELOPMENT

This is the Coq development for "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code".

Prerequisites

This version is known to compile with:

  • Coq 8.15.0
  • A development version of Iris (the version dev.2022-04-12.0.a3bed7ea)

Building from source

When building from source, we recommend to use opam (2.0.0 or newer) for installing the dependencies. This requires the following two repositories:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Once you got opam set up, run make build-dep to install the right versions of the dependencies.

Run make -jN to build the full development, where N is the number of your CPU cores.

To update, do git pull. After an update, the development may fail to compile because of outdated dependencies. To fix that, please run opam update followed by make build-dep.

Walkthrough

We have a walkthrough (walkthrough.md) of RustHornBelt's Coq development.

It explains in detail how to verify integer addition, model Vec, verify Vec::new, and verify mem::swap (featuring mutable borrows).

It is intended as a hands-on guide to our (huge) Coq development. In particular, it focuses on the things you need to know to reuse and extend the Coq development.

Structure

The theories folder, which contains the Coq mechanization, is structured as follows.

  • The folder util contains utility for basic concepts.
    • fancy_lists.v contains definitions, notation and lemmas for heterogeneous lists and related data types.
  • The folder prophecy contains the prophecy library, as well as the library for syntactic types.
  • The folder lifetime proves the rules of the lifetime logic, including derived constructions like (non-)atomic persistent borrows.
    • The subfolder model proves the core rules, which are then sealed behind a module signature in lifetime.v.
  • The folder lang contains the formalization of the lambda-Rust core language, including the theorem showing that programs with data races get stuck.
  • The folder typing defines the domain of semantic types and interpretations of all the judgments and also proves all typing rules.
    • type.v contains the definition of the notion of the semantic type.
    • programs.v defines the typing judgments for instructions and function bodies.
    • soundness.v contains the main soundness (adequacy) theorem of the type system.
    • The subfolder examples verifies some example Rust programs in Coq to conceptually demonstrate how functional verification works under the RustHorn-style translation.
    • The subfolder lib contains proofs for some APIs with unsafe code from the Rust standard library and some user crates. Some libraries are not yet verified, being commented out in _CoqProject.

Key Type-Spec Rules --- from the RustHornBelt Paper

The following table contains the location of every rule mentioned in the RustHornBelt paper. The filenames are spread across theories/typing/examples, theories/typing, theories/typing/lib (and its subfolders), and theories/prophecy.

Proof Rule File Lemma
Adequacy soundness.v type_soundness
Basic
MUTBOR derived_rules.v ty_uniq_bor
MUTREF-WRITE derived_rules.v ty_uniq_ref_write
MUTREF-BYE derived_rules.v ty_uniq_ref_bye
ENDLFT programs.v type_endlft
Prophecies
PROPH-INTRO prophecy.v proph_intro
PROPH-FRACT prophecy.v proph_tok_fractional
PROPH-IMPL prophecy.v proph_obs_impl
PROPH-MERGE prophecy.v proph_obs_and
PROPH-TRUE prophecy.v proph_obs_true
PROPH-RESOLVE prophecy.v proph_resolve
PROPH-SAT prophecy.v proph_obs_sat
Mutable Borrows
MUT-AGREE uniq_cmra.v uniq_agree
MUT-UPDATE uniq_cmra.v uniq_update
MUT-INTRO uniq_cmra.v uniq_intro
MUT-RESOLVE uniq_cmra.v uniq_resolve
Vec
push vec_pushpop.v vec_push_type
pop vec_pushpop.v vec_pop_type
index_mut vec_index.v vec_index_uniq_type
IterMut
iter_mut vec_slice.v vec_as_uniq_slice_type
next iter.v iter_uniq_next_type
inc_vec inc_vec.v inc_vec_type
Cell
new cell.v cell_new_type
get cell.v cell_get_type
set cell.v cell_set_type
inc_cell inc_cell.v inc_cell_type
Mutex
new mutex.v mutex_new_type
get_mut mutex.v mutex_get_uniq

Key Type(-Spec) Rules --- from the RustBelt Paper

The files in typing prove semantic versions of the proof rules given in the RustBelt paper. Notice that mutable borrows are called "unique borrows" in the Coq development.

Proof Rule File Lemma
T-bor-lft (for shr) shr_bor.v shr_subtype
T-bor-lft (for mut) uniq_bor.v uniq_subtype
C-subtype type_context.v subtype_tctx_incl
C-copy type_context.v copy_tctx_incl
C-split-bor (for shr) product_split.v tctx_split_shr_prod
C-split-bor (for mut) product_split.v tctx_split_uniq_prod
C-share borrow.v tctx_share
C-borrow borrow.v tctx_borrow
C-reborrow uniq_bor.v tctx_reborrow_uniq
Tread-own-copy own.v read_own_copy
Tread-own-move own.v read_own_move
Tread-bor (for shr) shr_bor.v read_shr
Tread-bor (for mut) uniq_bor.v read_uniq
Twrite-own own.v write_own
Twrite-bor uniq_bor.v write_uniq
S-num int.v type_int_instr
S-nat-leq int.v type_le_instr
S-new own.v type_new_instr
S-delete own.v type_delete_instr
S-deref programs.v type_deref_instr
S-assign programs.v type_assign_instr
F-consequence programs.v typed_body_impl
F-let programs.v type_let'
F-letcont cont.v type_cont
F-jump cont.v type_jump
F-newlft programs.v type_newlft
F-endlft programs.v type_endlft
F-call function.v type_call

Some of these lemmas are called something' because the version without the ' is a derived, more specialized form used together with our eauto-based solve_typing tactic. You can see this tactic in action in the examples subfolder.

Lifetime Logic Rules

The files in lifetime prove the lifetime logic, with the core rules being proven in the model subfolder and then sealed behind a module signature in lifetime.v.

Proof Rule File Lemma
LftL-begin model/creation.v lft_create
LftL-tok-fract model/primitive.v lft_tok_fractional
LftL-not-own-end model/primitive.v lft_tok_dead
LftL-end-persist model/definitions.v lft_dead_persistent
LftL-borrow model/borrow.v bor_create
LftL-bor-split model/bor_sep.v bor_sep
LftL-bor-acc lifetime.v bor_acc
LftL-bor-shorten model/primitive.v bor_shorten
LftL-incl-isect model/primitive.v lft_intersect_incl_l
LftL-incl-glb model/primitive.v lft_incl_glb
LftL-tok-inter model/primitive.v lft_tok_sep
LftL-end-inter model/primitive.v lft_dead_or
LftL-tok-unit model/primitive.v lft_tok_static
LftL-end-unit model/primitive.v lft_dead_static
LftL-reborrow lifetime.v rebor
LftL-bor-fracture frac_borrow.v bor_fracture
LftL-fract-acc frac_borrow.v frac_bor_atomic_acc
LftL-bor-na na_borrow.v bor_na
LftL-na-acc na_borrow.v na_bor_acc

For Developers: How to update the Iris dependency

  • Do the change in Iris, push it.
  • Wait for CI to publish a new Iris version on the opam archive, then run opam update iris-dev.
  • In lambdaRust, change the opam file to depend on the new version.
  • Run make build-dep (in lambdaRust) to install the new version of Iris. You may have to do make clean as Coq will likely complain about .vo file mismatches.