VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System (Artifact)

# Intro This contains the Rocq development validating the contributions of _VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System_. The artifact contains the following software: * An unmodified copy of [Iris](https://gitlab.mpi-sws.org/iris/iris) 4.3.0 * An unmodified copy of [stdpp](https://gitlab.mpi-sws.org/iris/stdpp) 1.11.0 * A modified copy of the [Leaf library](https://github.com/secure-foundations/leaf) * The VerusBelt source (main contribution of this artifact) * A docker image ready to build VerusBelt * A copy of [Verus](https://github.com/verus-lang/verus) source, release 0.2026.03.16.b1c2a95 * A docker image ready to run Verus Running or installing Verus is not strictly needed to evaluate the artifact, which primarily concerns the VerusBelt implementation in Rocq. The Verus source is primarily included to reference its source and docs. Information on installing Verus is included for completeness' sake; see `VERUS-IMPL.md` for more information. # Getting started Confirm that Rocq accepts all of the source files. This should take about 10-20 minutes.The easiest way should be with Docker, but we also provide instructions for a local install. ## With Docker Load the docker image: ```docker load -i verusbelt-docker-image.tar``` Open up a shell: ```docker run -it verusbelt /bin/bash``` From the shell, run: ```make -j4``` ## Local install First, install Rocq (formerly Coq) 8.20.0. You need to have [opam](https://opam.ocaml.org/) >= 2.0 installed. The simplest option is to create a fresh *local* opam switch with everything: ```opam updateopam switch create -y . ocaml-base-compiler.4.14.2opam pin coq 8.20.0eval $(opam env)``` then run: ```make -j4``` If you prefer to use your package manager to install Iris, rather than using the artifact'slocal copy, then install Iris 4.3.0 and stdpp 1.11.0: ```opam repo add rocq-released https://rocq-prover.github.io/opam/released/opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.gitopam pin coq-iris 4.3.0``` and run: ```make all_using_opam -j4``` # Detailed instructions for evaluation First, check that Rocq accepts the Leaf source code, as detailed above. Then, check that our source code supports the expected contributions. The contributions are: * Development of the Leaf Lifetime Logic (LeLiLo) * Development of the Points-To Cell Logic * The VerusBelt type-spec system, including: * Type soundness theorem * Typing rules for "standard" Rust types * Typing rules for a representative set of Verus proof-oriented types (**the primary contribution**) ## Leaf Lifetime Logic (LeLiLo) * Paper: Fig. 2* Rocq: * Source: `src/lambda_verus/lifetime/lifetime_full.v` * Doc: `doc/lifetime_full.html` Rules mentioned in the paper: | Name in paper | Name in Rocq ||--------------------|----------------------------------|| LeLiLo-Begin | `llftl_begin` || LeLiLo-Not-Own-End | `llftl_not_own_end` || LeLiLo-Tok-Inter | `llftl_tok_inter_and` || LeLiLo-End-Inter | `llftl_end_inter` || LeLiLo-Incl-Dead | `llftl_incl_dead_implies_dead` || LeLiLo-Incl-Guard | `llft_incl` (by definition) || LeLiLo-Shr-Borrow | `llftl_borrow_shared` || LeLiLo-Shr-Guard | by definition || LeLiLo-Shr-Pers | `llftl_borrow_shared_persistent` | Remarks: * The `&α shr P` notation in the paper is a paper-only notation which is defined (LeLiLo-Shr-Guard) to be `[α] guards P`. In the Rocq source, this is written: `@[α] &&{↑NllftG}&&> P`. * Often the notation appears with an additional `n` parameter: `@[α] &&{↑NllftG; n}&&> P`. The `n` parameter is the number of "laters" (▷) introduced when applying the guard. This detail is not discussed much in the paper (see footnote 3). ## Points-To Cell Logic * Paper: Fig. 4* Rocq: * Source: * `src/lambda_verus/util/non_atomic_cell_map.v` * `src/lambda_verus/lang/lifting.v` * Doc: * `doc/non_atomic_cell_map.html` * `doc/lifting.html` Notations: There are a number of notations for cell-points-to, for different levels of abstractionsand for all the different ways of specifying lists of cells.The `l @↦[ι][^cells] v` notation is closest to what's in the paper. | Rocq notation | Paper notation ||------------------------|--------------------------------------------------------|| `lc @↦[ι] cv` | `lc ↦ cv` || `lc @↦[ι][^ cells] cv` | `lc -[cells]↦ cv` || `l ↦ v` | `l ↦ v` || `l ↦! fv` | `l ↦ fv` || `l ↦[^ cells] v` | `l -[cells]↦ v` || `(l,cells) #↦_` | `l -[cells_0, ..., cells_(k-1)]↦ cells_k` || `(l,cells) #↦ v` | `cells_k ↦ v` (or `l ↦ v` if `cells` is empty) | Rules mentioned in the paper: | Name in paper | Name in Rocq | File ||----------------|------------------------------|-------------------------|| Cell-Sep | `pt_seq_app_sep` | `non_atomic_cell_map.v` || Cell-And | `pt_seq_app_and` | `non_atomic_cell_map.v` || Cell-Fresh | `pt_alloc_cell'` | `non_atomic_cell_map.v` || Heap-Read | `wp_read_na_guarded_cells_0` | `lifting.v` || Heap-Write1 | `wp_write_na` | `lifting.v` || Heap-Write2 | `wp_write_na_guarded_0` | `lifting.v` || Heap-Move-Cell | `wp_cell_move_na` | `lifting.v` | ## Type-spec soundness theorem * Paper: Sec. 3* Rocq: * Source: * `src/lambda_verus/typing/soundness.v` An example of instantiating the type-spec soundness theorem for a concrete piece of codecan be found in `src/lambda_verus/typing/examples/pcell_example.v`.This example file also documents how the checking of a type-spec in VerusBelt corresponds tothe checking done by actual Verus. ## Semantic types * Paper: Sec. 3.1* Rocq: * Source: * `src/lambda_verus/typing/type.v` The `type` record is used to define a semantic type. Types are parameterized by `𝔄` whichrepresents the interpreation sort.This record is instantiated for all the types we care about in VerusBelt The most important fields of this record are the `ty_gho` and `ty_phys` functions, which correspondto [[T]].own and [[T]].phys from the paper. Also of note are: * `ty_size`: the size of the type * `ty_lfts`: lifetimes the type is included in (e.g., `&'a T` is included in `'a`) * `ty_gho_pers`: the "persistent part of" `ty_gho`. Finally, there are a bunch of well-formedness conditions. ## Typing rules Typing rules for standard Rust types largely covers the same feature set as the prior work(RustHornBelt) but are slightly modified for the following reasons: * Predicates require two additional parameters: the `mask` (see Sec. 4) and the `π` parameter of type `ProphAsn` (see Sec. 5.1). * Interpretation sorts have a little more information in them, e.g., a `box ty` is interpretted as `(l, x)` where `l` is the address of the box. Below, we detail where to find the most important typing rules. ### Standard Rust types Key typing rules: * `src/lambda_verus/typing/` * `programs.v` * `type_newlft`: Starting a lifetime * `type_endlft`: Ending a lifetime * `type_assign`: Assignment from one location to another * `int.v`: Int type * `bool.v`: Bool type * `product.v`: Product types (tuples / structs) * `sum.v`: Sum types (enums) * `own.v`: Box types * `shr_bor.v`: Shared references (`&T`) * `uniq_bor.v`: Unique reference (`&mut T`) * `borrow.v`: * `type_uniqbor_instr`: Create a new borrow * `type_share`: Unique borrow -> shared borrow * `tcx_reborrow_uniq`: Reborrow * `type_deref_uniq_own`: Unique borrow from behind a `Box` * `type_deref_shr_own`: Shared borrow from behind a `Box` * `type_deref_uniq_uniq`: `&mut &mut T` -> `&mut T` * `type_deref_shr_uniq`: `& &mut T` -> `&T` * `product_split.v`: * `tctx_split_shr_prod`: `&(T, U)` to `&T` and `&U` * `type_split_uniq_bor_instr` `&mut (T, U)` to `&mut T` and `&mut U` * `type_sum.v`: * `type_case_shr_inner`: Match on enum and take shared reference to contents * `type_case_uniq_inner`: Match on enum and take unique reference to contents * `function.v` * `type_call`, `type_letcall`: Calling a function * `type_fn`, `type_fnrec`: typing a function value * `fixpoint.v` - Fixpoint machinery for recursive types (see `src/lambda_verus/typing/examples/list.v` for an example) ### Verus proof-oriented types In what follows, we will cover the typing rules for Verus proof-oriented types,which together compose the primary contribution of the VerusBelt.Since these types are unusual and not well known, we will also detail the relationship betweenthe type-spec rules and the Verus source. Most Verus proof-oriented types are declared in the "Verus standard library", `vstd`, withindividual operations specified as axiomatic functions with a `requires` and `ensures` clause.The ideal is to have a type-spec theorem in VerusBelt for every axiom in Verus;in practice, the relationship is more complex due to limitations or simplifications,which we detail below. (This goes both directions; sometimes the VerusBelt specs are _more_ general.)VerusBelt focuses on the proof-oriented types; we do not attempt toverify, e.g., Rust stdlib container types, which are also axiomatized in vstd. Other notes: * In VerusBelt, many variables (e.g., local variables, function arguments) need to be boxed where they wouldn't be in Rust source. Following RustBelt, these boxes appear in the "de-sugaring". Thus, many VerusBelt specifications may have extra `box` or `own` types. * VerusBelt's `tr