Skip to content
Snippets Groups Projects
Select Git revision
  • masters/weak_mem protected
  • masters/rusthornbelt protected
  • master default protected
  • ci/ike/frame_exist
  • ralf/prop-level-wand
  • msammler/new-contractive
  • xldenis/pldi-submission
  • xldenis/smallvec-push
  • refmut_sync
  • robbert/sprop
  • ci/pinning
  • xldenis/option
  • robbert/Z_of_nat
  • xldenis/type-sum
  • yusuke/tlist_for_prophecy
  • msammler/rustverify_talk
  • gpirlea/pin_semantic
  • rusthornbelt
  • ci/janno/strict-tc-resolution
  • step_indexing_controlled_by_ghosts
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
Compare
Name Last commit Last update
theories
.gitignore
.gitlab-ci.yml
LICENSE
Makefile
Missing.md
README.md
_CoqProject
opam
README.md

RBrlx (RustBelt Relaxed) COQ DEVELOPMENT

This is the Coq development accompanying RBrlx.

Prerequisites

This version is known to compile with:

  • Coq 8.10.2 / 8.11.0
  • A development version of GPFSL.

The easiest way to install the correct versions of the dependencies is through opam (2.0.0 or newer). You will need the Coq and Iris opam 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.

Updating

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

Building Instructions

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

Structure

  • The folder lang contains the formalization of abstract specifications for several data structures in the ORC11 relaxed memory semantics. These data structures are the building blocks for the RBrlx's version of Rust libraries.
    • The repository ORC11 formalizes the operational relaxed memory semantics employed by RBrlx.
    • The repository GPFSL formalizes the actual language of RBrlx, as well as the logic for general verification of programs written that language. The language combines ORC11 with an CPS-style expression language (following that of lambda-Rust).
  • 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 logic proves the surface-level rules of GPFSL atomic-borrows-based protocols. These rules combine GPFSL's raw rules with the lifetime logic rules for atomic borrows.
  • The folder typing defines the domain of semantic types, interpretations of all the judgments, as well as proofs of all typing rules.
    • type.v contains the definition of a semantic type.
    • programs.v defines the typing judgments for instructions and function bodies.
    • soundness.v contains the main soundness theorem of the type system.
    • The subfolder examples shows how the examples from the technical appendix can be type-checked in Coq.
    • The subfolder lib contains proofs of safety of some unsafely implement types from the Rust standard library and some user crates: Cell, RefCell, Rc, Arc, Mutex, RwLock, mem::swap, thread::spawn, take_mut::take, alias::once as well as converting &&T to &Box<T>.

Where to Find the Proof Rules From the Paper

Type System Rules

The files in typing prove semantic versions of the proof rules given in the original 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_mono
T-bor-lft (for mut) uniq_bor.v uniq_mono
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_prod2
C-split-bor (for mut) product_split.v tctx_split_uniq_prod2
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_mono
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. The interface of the core lifetime logic is in lifetime_sig.v.

Proof Rule File Lemma
LftL-begin model/creation.v lft_create
LftL-tok-fract model/primitive.v lft_tok_fractional
LftL-tok-fract-obj model/primitive.v lft_tok_split_obj
LftL-tok-comp model/primitive.v lft_tok_sep
LftL-tok-unit model/primitive.v lft_tok_static
LftL-not-own-end model/primitive.v lft_tok_dead
LftL-end-comp model/primitive.v lft_dead_or
LftL-end-unit model/primitive.v lft_dead_static
LftL-borrow model/borrow.v bor_create
LftL-bor-sep model/bor_sep.v bor_sep, bor_combine
LftL-bor-fake model/faking.v bor_fake
LftL-bor-acc-strong model/accessors.v bor_acc_strong
LftL-bor-acc-atomic-strong model/accessors.v bor_acc_atomic_strong
LftL-bor-idx model/primitive.v bor_unfold_idx
LftL-idx-shorten model/primitive.v idx_bor_shorten
LftL-idx-acc model/accessors.v idx_bor_acc
LftL-idx-bor-unnest model/reborrow.v idx_bor_unnest
LftL-idx-bor-iff model/reborrow.v idx_bor_iff
LftL-bor-in-at model/in_at_borrow.v in_at_bor_share
LftL-in-at-acc model/in_at_borrow.v in_at_bor_acc
LftL-in-at-shorten model/in_at_borrow.v in_at_bor_shorten
LftL-in-at-iff model/in_at_borrow.v in_at_bor_iff
LftL-incl-isect model/primitive.v lft_intersect_incl_l
LftL-incl-glb model/primitive.v lft_incl_glb
LftL-fract-lincl frac_borrow.v frac_bor_lft_incl
LftL-bor-shorten lifetime.v bor_shorten
LftL-reborrow lifetime.v rebor
LftL-bor-unnest lifetime.v bor_unnest
LftL-bor-acc-cons lifetime.v bor_acc_cons
LftL-bor-acc lifetime.v bor_acc
LftL-bor-freeze lifetime.v bor_exists
LftL-bor-iff lifetime.v bor_iff
LftL-bor-at at_borrow.v at_bor_share
LftL-at-acc at_borrow.v at_bor_acc
LftL-at-shorten at_borrow.v at_bor_shorten
LftL-at-iff at_borrow.v at_bor_iff
LftL-bor-na na_borrow.v bor_na
LftL-na-acc na_borrow.v na_bor_acc
LftL-na-shorten na_borrow.v na_bor_shorten
LftL-na-iff na_borrow.v na_bor_iff
LftL-bor-fracture frac_borrow.v bor_fracture'
LftL-fract-acc frac_borrow.v frac_bor_acc
LftL-fract-shorten frac_borrow.v frac_bor_shorten
LftL-fract-iff frac_borrow.v frac_bor_iff

Verification of Full Arc

We do not have the Core Arc example (Section 3.3 of the RBrlx paper) in Coq. Instead, we have the Full Arc example (Section 5.3 of the RBrlx paper, also Section 6 of its technical appendix).

The verification of Full Arc is split into 2 parts:

  1. Verifying Full Arc with respect to some abstract specification. This is done in lang/arc.v, with the help of a CMRA (PCM) defined in lang/arc_cmra.v. The specification is proven in the *_spec lemmas. More comments can be found in the aforementioned files.
  2. Verifying that the abstract specification implies the semantics interpretation of the type of Arc and Weak. This can be found in typing/lib/arc.v. In this file,
    • the Program Definition arc (ty : type) and Program Definition weak (ty : type) are the interpretations of the Arc<ty> and Weak<ty> types, respectively.
    • arc_send, arc_sync, weak_send, weak_sync prove that both Arc<ty> and Weak<ty> correctly implement the Send and Sync traits.
    • The *_type lemmas prove that each function semantically satisfies its syntactic type.

For Developers: How to update the GPFSL dependency

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