Add comments on corresponding Rust methods and tweak some names

README.md

@@ -13,7 +13,7 @@ This version is known to compile with:
 ## 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:
+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
@@ -24,37 +24,37 @@ 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`
+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`.
 
 ## Structure
 
-* The folder [util](theories/util) contains utility for basic concepts.
-  * [fancy_lists.v](theories/util/fancy_lists.v) contains definitions, notation
+- The folder [util](theories/util) contains utility for basic concepts.
+  - [fancy_lists.v](theories/util/fancy_lists.v) contains definitions, notation
     and lemmas for heterogeneous lists and related data types.
-* The folder [prophecy](theories/prophecy) contains the prophecy library,
+- The folder [prophecy](theories/prophecy) contains the prophecy library,
   as well as the library for syntactic types.
-* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
+- The folder [lifetime](theories/lifetime) proves the rules of the lifetime
   logic, including derived constructions like (non-)atomic persistent borrows.
-  * The subfolder [model](theories/lifetime/model) proves the core rules, which
+  - The subfolder [model](theories/lifetime/model) proves the core rules, which
     are then sealed behind a module signature in
     [lifetime.v](theories/lifetime/lifetime.v).
-* The folder [lang](theories/lang) contains the formalization of the lambda-Rust
+- The folder [lang](theories/lang) contains the formalization of the lambda-Rust
   core language, including the theorem showing that programs with data races get
   stuck.
-* The folder [typing](theories/typing) defines the domain of semantic types and
+- The folder [typing](theories/typing) defines the domain of semantic types and
   interpretations of all the judgments and also proves all typing rules.
-  * [type.v](theories/typing/type.v) contains the definition of the notion
+  - [type.v](theories/typing/type.v) contains the definition of the notion
     of the semantic type.
-  * [programs.v](theories/typing/programs.v) defines the typing judgments for
+  - [programs.v](theories/typing/programs.v) defines the typing judgments for
     instructions and function bodies.
-  * [soundness.v](theories/typing/soundness.v) contains the main soundness
+  - [soundness.v](theories/typing/soundness.v) contains the main soundness
     (adequacy) theorem of the type system.
-  * The subfolder [examples](theories/typing/examples) verifies some example
+  - The subfolder [examples](theories/typing/examples) verifies some example
     Rust programs in Coq to conceptually demonstrate how functional verification
     works under the RustHorn-style translation.
-  * The subfolder [lib](theories/typing/lib) contains proofs for some APIs
+  - The subfolder [lib](theories/typing/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`.
 
@@ -93,7 +93,7 @@ The filenames are spread across `theories/typing/examples`, `theories/typing`, `
 | `pop`               | `vec_pushpop.v`   | `vec_pop_type`           |
 | `index_mut`         | `vec_index.v`     | `vec_index_uniq_type`    |
 | **`IterMut`**       |                   |                          |
-| `iter_mut`          | `vec_slice.v`     | `vec_to_uniq_slice_type` |
+| `iter_mut`          | `vec_slice.v`     | `vec_as_slice_uniq_type` |
 | `next`              | `iter.v`          | `iter_uniq_next_type`    |
 | `inc_vec`           | `inc_vec.v`       | `inc_vec_type`           |
 | **`Cell`**          |                   |                          |
@@ -103,48 +103,48 @@ The filenames are spread across `theories/typing/examples`, `theories/typing`, `
 | `inc_cell`          | `inc_cell.v`      | `inc_cell_type`          |
 | **`Mutex`**         |                   |                          |
 | `new`               | `mutex.v`         | `mutex_new_type`         |
-| `get_mut`           | `mutex.v`         | `mutex_get_mut`          |
+| `get_mut`           | `mutex.v`         | `mutex_get_uniq`          |
 
 ### Key Type(-Spec) Rules --- from the RustBelt Paper
 
 The files in [typing](theories/typing) prove semantic versions of the proof
-rules given in the *RustBelt* paper.  Notice that mutable borrows are called
+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             |
+| 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
+`solve_typing` tactic. You can see this tactic in action in the
 [examples](theories/typing/examples) subfolder.
 
 ### Lifetime Logic Rules
@@ -155,7 +155,7 @@ then sealed behind a module signature in
 [lifetime.v](theories/lifetime/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         |
@@ -178,10 +178,10 @@ then sealed behind a module signature in
 
 ## 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
+- 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.
+- 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.

theories/typing/examples/inc_vec.v

@@ -10,7 +10,7 @@ Section code.
 
   Definition inc_vec : val :=
     fn: ["v"] :=
-      let: "iter_mut" := vec_to_slice in
+      let: "iter_mut" := vec_as_slice in
       letcall: "it" := "iter_mut" ["v"] in
       withcont: "k":
         withcont: "loop":
@@ -40,7 +40,7 @@ Section code.
       (λ post '-[(v, v')], v' = map (λ e, e + 5) v → post ()).
   Proof.
     eapply type_fn; [apply _|]=>/= α ϝ ret [v[]]. simpl_subst. via_tr_impl.
-    { iApply type_val; [apply (vec_to_uniq_slice_type int)|]. intro_subst.
+    { iApply type_val; [apply (vec_as_slice_uniq_type int)|]. intro_subst.
       iApply type_letcall; [solve_typing|solve_extract|solve_typing|..].
       iIntros (iter). simpl_subst.
       iApply (type_cont [] (λ _, +[iter ◁ _]) (λ (post : ()%ST → _) _, post ())).

theories/typing/lib/cell.v

@@ -9,6 +9,7 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section cell.
   Context `{!typeG Σ}.
 
+  (* Rust's cell::Cell<T> *)
   Program Definition cell {𝔄} (ty: type 𝔄) : type (predₛ 𝔄) := {|
     ty_size := ty.(ty_size);  ty_lfts := ty.(ty_lfts);  ty_E := ty.(ty_E);
     ty_own Φπ _ tid vl := ∃Φ (vπ: proph 𝔄) d, ⌜Φπ = const Φ⌝ ∗
@@ -139,6 +140,7 @@ Section cell.
 
   Definition cell_new: val := fn: ["x"] := return: ["x"].
 
+  (* Rust's Cell::new *)
   Lemma cell_new_type {𝔄} (ty: type 𝔄) Φ :
     typed_val cell_new (fn(∅; ty) → cell ty) (λ post '-[a], Φ a ∧ post Φ).
   Proof.
@@ -167,6 +169,7 @@ Section cell.
 
   Definition cell_into_inner: val := fn: ["x"] := return: ["x"].
 
+  (* Rust's Cell::into_inner *)
   Lemma cell_into_inner_type {𝔄} (ty: type 𝔄) :
     typed_val cell_into_inner (fn(∅; cell ty) → ty)
       (λ post '-[Φ], ∀a: 𝔄, Φ a → post a).
@@ -238,6 +241,7 @@ Section cell.
 
   Definition cell_from_uniq: val := fn: ["x"] := Skip;; return: ["x"].
 
+  (* Rust's Cell::from_mut *)
   (* In this rule, we lose the prophecy information of the input.
     We need a stronger model of prophecy to know that
     the prophetic value of the input satisfies [Φ']. *)
@@ -274,6 +278,7 @@ Section cell.
 
   Definition cell_get_uniq: val := fn: ["x"] := Skip;; return: ["x"].
 
+  (* Rust's Cell::get_mut *)
   Lemma cell_get_uniq_type {𝔄} Ψ (ty: type 𝔄) :
     typed_val cell_get_uniq (fn<α>(∅; &uniq{α} (cell ty)) → &uniq{α} (!{Ψ} ty))
       (λ post '-[(Φ, Φ')], ∀a a': 𝔄, Φ a → Φ' = Ψ → Ψ a ∧ post (a, a')).
@@ -368,6 +373,7 @@ Section cell.
 
   (* Interestingly, this is syntactically well-typed: we do not need
      to enter the model. *)
+  (* Rust's Cell::get *)
   Lemma cell_get_type {𝔄} (ty: type 𝔄) `{!Copy ty} :
     typed_val (cell_get ty) (fn<α>(∅; &shr{α} (cell ty)) → ty)
       (λ post '-[Φ], ∀a: 𝔄, Φ a → post a).
@@ -389,6 +395,7 @@ Section cell.
       "c'" <-{ty.(ty_size)} !"x";; delete [ #ty.(ty_size); "x"];;
       return: [new [ #0]].
 
+  (* Rust's Cell::set *)
   Lemma cell_set_type {𝔄} (ty: type 𝔄) :
     typed_val (cell_set ty) (fn<α>(∅; &shr{α} (cell ty), ty) → ())
       (λ post '-[Φ; a], Φ a ∧ post ()).
@@ -429,6 +436,7 @@ Section cell.
       "c'" <-{ty.(ty_size)} !"x";;
       delete [ #ty.(ty_size); "x"];; return: ["r"].
 
+  (* Rust's Cell::replace *)
   Lemma cell_replace_type {𝔄} (ty: type 𝔄) :
     typed_val (cell_replace ty) (fn<α>(∅; &shr{α} (cell ty), ty) → ty)
       (λ post '-[Φ; a], Φ a ∧ ∀a': 𝔄, Φ a' → post a').

theories/typing/lib/list.v

@@ -19,6 +19,9 @@ Section list.
     <{psum_to_list: (Σ! [(); (𝔄 * listₛ 𝔄)])%ST → listₛ 𝔄}> (Σ! +[(); ty * box ty'])%T.
 End list.
 
+(* In Rust:
+  enum List<T> { Nil, Cons(T, Box<List<T>>) }
+*)
 Notation list_ty ty := (fix_ty (list_map ty)).
 Notation list_cons_ty ty := (ty * box (list_ty ty))%T.
 Notation list_xsum_ty ty := (Σ! +[(); list_cons_ty ty])%T.

theories/typing/lib/maybe_uninit.v

@@ -22,6 +22,7 @@ Section maybe_uninit.
       iRight. iExists vπ'. by iSplit.
   Qed.
 
+  (* Rust's mem::MaybeUninit<T> *)
   Program Definition maybe_uninit {𝔄} (ty: type 𝔄) : type (optionₛ 𝔄) := {|
     ty_size := ty.(ty_size);  ty_lfts := ty.(ty_lfts);  ty_E := ty.(ty_E);
     ty_own vπ d tid vl :=
@@ -162,6 +163,7 @@ Section typing.
     eqtype E L ty ty' f g → eqtype E L (? ty) (? ty') (option_map f) (option_map g).
   Proof. move=> [??]. split; by apply maybe_uninit_subtype. Qed.
 
+  (* Rust's MaybeUninit::new *)
   Lemma uninit_to_maybe_uninit {𝔄} (ty: type 𝔄) E L :
     subtype E L (↯ ty.(ty_size)) (? ty) (const None).
   Proof.
@@ -169,6 +171,7 @@ Section typing.
     iSplit; iIntros "!>** /="; iLeft; by iSplit.
   Qed.
 
+  (* Rust's MaybeUninit::uninit *)
   Lemma into_maybe_uninit {𝔄} (ty: type 𝔄) E L : subtype E L ty (? ty) Some.
   Proof.
     iIntros "*_!>_". iSplit; [done|]. iSplit; [by iApply lft_incl_refl|].
@@ -186,6 +189,7 @@ Section typing.
       iRight. iExists vπ''. by iFrame.
   Qed.
 
+  (* Rust's MaybeUninit::assume_uninit *)
   Lemma tctx_unwrap_maybe_uninit {𝔄 𝔅l} (ty: type 𝔄) E L (T: tctx 𝔅l) p :
     tctx_incl E L (p ◁ ? ty +:: T) (p ◁ ty +:: T)
       (λ post '(o -:: bl), match o with
@@ -213,6 +217,7 @@ Section typing.
     iFrame "⧖ †". iNext. iExists _. iFrame.
   Qed.
 
+  (* Rust's MaybeUninit::assume_uninit_ref *)
   Lemma tctx_unwrap_shr_maybe_uninit {𝔄 𝔅l} (ty: type 𝔄) κ E L (T: tctx 𝔅l) p :
     tctx_incl E L (p ◁ &shr{κ} (? ty) +:: T) (p ◁ &shr{κ} ty +:: T)
       (λ post '(o -:: bl), match o with
@@ -226,6 +231,7 @@ Section typing.
     iExists _, _. iSplit; [done|]. by iFrame "⧖".
   Qed.
 
+  (* Rust's MaybeUninit::assume_uninit_mut *)
   Lemma tctx_unwrap_uniq_maybe_uninit {𝔄 𝔅l} (ty: type 𝔄) κ E L (T: tctx 𝔅l) p :
     lctx_lft_alive E L κ →
     tctx_incl E L (p ◁ &uniq{κ} (? ty) +:: T) (p ◁ &uniq{κ} ty +:: T)

theories/typing/lib/mutex/mutex.v

@@ -57,6 +57,7 @@ Section mutex.
       rewrite heap_mapsto_vec_cons. iFrame "↦b ↦". iExists _, _, _, _, _. by iFrame.
   Qed.
 
+  (* Rust's sync::Mutex<T> *)
   Program Definition mutex {𝔄} (ty: type 𝔄) : type (predₛ 𝔄) := {|
       ty_size := 1 + ty.(ty_size);  ty_lfts := ty.(ty_lfts);  ty_E := ty.(ty_E);
       ty_own Φπ _ tid vl := ∃Φ (b: bool) vl' (vπ: proph 𝔄) d,
@@ -154,6 +155,7 @@ Section mutex.
     eqtype E L ty ty' f g → eqtype E L (mutex ty) (mutex ty') (.∘ g) (.∘ f).
   Proof. move=> [??]. split; by (eapply mutex_subtype; [split; apply _|]). Qed.
 
+  (* Rust's Mutex::new *)
   Definition mutex_new {𝔄} (ty: type 𝔄) : val :=
     fn: ["x"] :=
       let: "m" := new [ #(mutex ty).(ty_size)] in
@@ -185,6 +187,7 @@ Section mutex.
     by iApply proph_obs_impl; [|done]=>/= ?[? _].
   Qed.
 
+  (* Rust's Mutex::into_inner *)
   Definition mutex_into_inner {𝔄} (ty: type 𝔄) : val :=
     fn: ["m"] :=
       let: "x" := new [ #ty.(ty_size)] in
@@ -212,7 +215,8 @@ Section mutex.
     rewrite/= freeable_sz_full. iFrame "†x". iNext. iExists _. iFrame.
   Qed.
 
-  Definition mutex_get_mut: val :=
+  (* Rust's Mutex::get_mut *)
+  Definition mutex_get_uniq: val :=
     fn: ["m"] :=
       let: "m'" := !"m" in
       "m" <- ("m'" +ₗ #1);;
@@ -220,8 +224,8 @@ Section mutex.
 
   (* The final invariant of [&uniq{α} (mutex ty)] should be trivial,
     because [&uniq{α} ty] does not restrict the target value *)
-  Lemma mutex_get_mut_type {𝔄} (ty: type 𝔄) :
-    typed_val mutex_get_mut (fn<α>(∅; &uniq{α} (mutex ty)) → &uniq{α} ty)
+  Lemma mutex_get_uniq_type {𝔄} (ty: type 𝔄) :
+    typed_val mutex_get_uniq (fn<α>(∅; &uniq{α} (mutex ty)) → &uniq{α} ty)
       (λ post '-[(Φ, Φ')], ∀a a': 𝔄, Φ a → Φ' = const True → post (a, a')).
   Proof.
     eapply type_fn; [apply _|]=>/= α ??[m[]]. simpl_subst.

theories/typing/lib/mutex/mutexguard.v

@@ -41,6 +41,7 @@ Section mutexguard.
       rewrite heap_mapsto_vec_singleton. iFrame "↦". iExists _, _. by iFrame.
   Qed.
 
+  (* Rust's sync::MutexGuard<'a, T> *)
   Program Definition mutexguard {𝔄} (κ: lft) (ty: type 𝔄) : type (predₛ 𝔄) := {|
     ty_size := 1;  ty_lfts := κ :: ty.(ty_lfts);  ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
     (* One logical step is required for [ty_share] *)
@@ -193,6 +194,7 @@ Section mutexguard.
       letalloc: "g" <- "m" in
       delete [ #1; "bm"];; return: ["g"].
 
+  (* Rust's Mutex::lock *)
   Lemma mutex_lock_type {𝔄} (ty: type 𝔄) :
     typed_val mutex_lock (fn<α>(∅; &shr{α} (mutex ty)) → mutexguard α ty)
       (λ post '-[Φ], post Φ).
@@ -222,6 +224,7 @@ Section mutexguard.
       letalloc: "r" <- "m" +ₗ #1 in
       delete [ #1; "g"];; return: ["r"].
 
+  (* Rust's MutexGuard::deref_mut *)
   Lemma mutexguard_deref_uniq_type {𝔄} Ψ (ty: type 𝔄) :
     typed_val mutexguard_deref
       (fn<(α, β)>(∅; &uniq{α} (mutexguard β ty)) → &uniq{α} (!{Ψ} ty))
@@ -286,6 +289,7 @@ Section mutexguard.
       iApply proph_obs_impl; [|done]=>/= ?[[[_[Eqv _]]_]?]. by apply Eqv.
   Qed.
 
+  (* Rust's MutexGuard::deref *)
   Lemma mutexguard_deref_shr_type {𝔄} (ty: type 𝔄) :
     typed_val mutexguard_deref
       (fn<(α, β)>(∅; &shr{α} (mutexguard β ty)) → &shr{α} ty)
@@ -328,6 +332,7 @@ Section mutexguard.
       release [!"g"];; delete [ #1; "g"];;
       return: [new [ #0]].
 
+  (* Rust's MutexGuard::drop *)
   Lemma mutexguard_drop_type {𝔄} (ty: type 𝔄) :
     typed_val mutexguard_drop (fn<α>(∅; mutexguard α ty) → ())
       (λ post '-[_], post ()).

theories/typing/lib/option.v

@@ -15,6 +15,7 @@ Proof. split; fun_ext; case=>//; by case. Qed.
 Section option.
   Context `{!typeG Σ}.
 
+  (* Rust's Option<T> *)
   Definition option_ty {𝔄} (ty: type 𝔄) : type (optionₛ 𝔄) :=
     <{psum_to_option: (Σ! [(); 𝔄])%ST → optionₛ 𝔄}> (Σ! +[(); ty])%T.
 
@@ -50,7 +51,7 @@ Section option.
   Definition none := 0%nat.
   Definition some := 1%nat.
 
-  Definition option_as_mut : val :=
+  Definition option_as_uniq : val :=
     fn: ["o"] :=
       let: "o'" := !"o" in let: "r" := new [ #2] in
     withcont: "k":
@@ -60,8 +61,9 @@ Section option.
     cont: "k" [] :=
       delete [ #1; "o"];; return: ["r"].
 
-  Lemma option_as_mut_type {𝔄} (ty: type 𝔄) :
-    typed_val option_as_mut
+  (* Rust's Option::as_mut *)
+  Lemma option_as_uniq_type {𝔄} (ty: type 𝔄) :
+    typed_val option_as_uniq
       (fn<α>(∅; &uniq{α} (option_ty ty)) → option_ty (&uniq{α} ty))
       (λ (post: pred' (optionₛ (_*_))) '-[a], match a with
         | (Some a, Some a') => post (Some (a, a'))
@@ -97,6 +99,7 @@ Section option.
         delete [ #(S ty.(ty_size)); "o"];; delete [ #ty.(ty_size); "def"];;
         return: ["r"]].
 
+  (* Rust's Option::unwrap_or *)
   Lemma option_unwrap_or_type {𝔄} (ty: type 𝔄) :
     typed_val (option_unwrap_or ty) (fn(∅; option_ty ty, ty) → ty)
       (λ post '-[o; d], match o with Some a => post a | None => post d end).
@@ -121,6 +124,7 @@ Section option.
       ; letalloc: "r" <-{ty.(ty_size)} !("o" +ₗ #1) in
         delete [ #(S ty.(ty_size)); "o"];; return: ["r"]].
 
+  (* Rust's Option::unwrap *)
   Lemma option_unwrap_type {𝔄} (ty: type 𝔄) :
     typed_val (option_unwrap ty) (fn(∅; option_ty ty) → ty)
       (λ post '-[o], match o with Some a => post a | None => False end).

theories/typing/lib/panic.v

@@ -18,6 +18,7 @@ Section panic.
   Definition panic: val :=
     fn: [] := stuck_term.
 
+  (* Rust's panic! *)
   Lemma panic_type: typed_val panic (fn(∅) → ∅) (λ _ _, False).
   Proof.
     eapply type_fn; [apply _|]=>/= *.
@@ -25,6 +26,7 @@ Section panic.
     iMod (proph_obs_false with "PROPH Obs") as "[]"; [done|move=> ?[]].
   Qed.
 
+  (* Rust's assert! *)
   Lemma type_assert_instr E L p :
     typed_instr E L +[p ◁ bool_ty] (assert: p) (const +[])
       (λ post '-[b], if b then post -[] else False).

theories/typing/lib/slice/array_slice.v

@@ -8,15 +8,16 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section array_slice.
   Context `{!typeG Σ}.
 
-  Definition array_to_slice (n: nat) : val :=
+  Definition array_as_slice (n: nat) : val :=
     fn: ["ba"] :=
       let: "a" := !"ba" in delete [ #1; "ba"];;
       let: "r" := new [ #2] in
       "r" <- "a";; "r" +ₗ #1 <- #n;;
       return: ["r"].
 
-  Lemma array_to_uniq_slice_type {𝔄} n (ty: type 𝔄) :
-    typed_val (array_to_slice n) (fn<α>(∅; &uniq{α} [ty;^ n]) → uniq_slice α ty)
+  (* Rust's [T; n]::as_mut_slice *)
+  Lemma array_as_slice_uniq_type {𝔄} n (ty: type 𝔄) :
+    typed_val (array_as_slice n) (fn<α>(∅; &uniq{α} [ty;^ n]) → uniq_slice α ty)
       (λ post '-[(al, al')], length al' = length al → post (zip al al')).
   Proof.
     eapply type_fn; [apply _|]=>/= α ??[ba[]]. simpl_subst.

theories/typing/lib/slice/iter.v

@@ -9,6 +9,7 @@ Section iter.
   Context `{!typeG Σ}.
 
   (** We model the unique iterator the same as the unique slice *)
+  (* Rust's IterMut<'a, T> *)
   Definition iter_uniq {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ (𝔄 * 𝔄)) :=
     uniq_slice κ ty.
 
@@ -23,6 +24,7 @@ Section iter.
         "it" <- "l" +ₗ #ty.(ty_size);; "it" +ₗ #1 <- "len" - #1;;
         let: "r" := new [ #2] in "r" <-{Σ 1} "l";; return: ["r"].
 
+  (* Rust's IterMut::next *)
   Lemma iter_uniq_next_type {𝔄} (ty: type 𝔄) :
     typed_val (iter_next ty)
       (fn<(α, β)>(∅; &uniq{β} (iter_uniq α ty)) → option_ty (&uniq{α} ty))
@@ -97,6 +99,7 @@ Section iter.
         let: "l'" := !"it" +ₗ "len'" * #ty.(ty_size) in
         let: "r" := new [ #2] in "r" <-{Σ 1} "l'";; return: ["r"].
 
+  (* Rust's IterMut::next_back *)
   Lemma iter_uniq_next_back_type {𝔄} (ty: type 𝔄) :
     typed_val (iter_next_back ty)
       (fn<(α, β)>(∅; &uniq{β} (iter_uniq α ty)) → option_ty (&uniq{α} ty))

theories/typing/lib/slice/slice_basic.v

@@ -87,6 +87,7 @@ Section slice_basic.
       letalloc: "r" <- !("s" +ₗ #1) in
       return: ["r"].
 
+  (* Rust's [T]::len *)
   Lemma uniq_slice_len_type {𝔄} (ty: type 𝔄) :
     typed_val slice_len (fn<(α, β)>(∅; &shr{β} (uniq_slice α ty)) → int)
       (λ post '-[aal], post (length aal)).

theories/typing/lib/slice/slice_split.v

@@ -19,7 +19,8 @@ Section slice_split.
       "r" +ₗ #2 <- "l" +ₗ "i" * #ty.(ty_size);; "r" +ₗ #3 <- "len" - "i";;
       return: ["r"].
 
-  Lemma uniq_slice_split_at_type {𝔄} (ty: type 𝔄) :
+  (* Rust's split_at_mut *)
+  Lemma slice_split_at_uniq_type {𝔄} (ty: type 𝔄) :
     typed_val (slice_split_at ty)
       (fn<α>(∅; uniq_slice α ty, int) → uniq_slice α ty * uniq_slice α ty)
       (λ post '-[aal; z],

theories/typing/lib/slice/uniq_slice.v

@@ -22,6 +22,7 @@ Section uniq_slice.
       iExists _, _, _, _. by iFrame.
   Qed.
 
+  (* Rust's &'a mut [T] *)
   Program Definition uniq_slice {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ (𝔄 * 𝔄)) := {|
     ty_size := 2;  ty_lfts := κ :: ty.(ty_lfts);  ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
     ty_own vπ d tid vl := κ ⊑ ty.(ty_lft) ∗

theories/typing/lib/smallvec/smallvec.v

@@ -71,6 +71,7 @@ Section smallvec.
         iExists false, _, _, _, _, _=>/=. by iFrame.
   Qed.
 
+  (* Rust's SmallVec<[T; n]> *)
   (* For simplicity, it always has the location and capacity *)
   Program Definition smallvec {𝔄} (n: nat) (ty: type 𝔄) : type (listₛ 𝔄) := {|
     ty_size := 4 + n * ty.(ty_size);

theories/typing/lib/smallvec/smallvec_basic.v

@@ -104,6 +104,7 @@ Section smallvec_basic.
       "r" +ₗ #2 <- #0;; "r" +ₗ #3 <- #0;;
       return: ["r"].
 
+  (* Rust's SmallVec::new *)
   Lemma smallvec_new_type {𝔄} n (ty: type 𝔄) :
     typed_val (smallvec_new n ty) (fn(∅) → smallvec n ty) (λ post _, post []).
   Proof.
@@ -123,7 +124,7 @@ Section smallvec_basic.
     by rewrite repeat_length.
   Qed.
 
-  Definition smallvec_delete {𝔄} n (ty: type 𝔄) : val :=
+  Definition smallvec_drop {𝔄} n (ty: type 𝔄) : val :=
     fn: ["v"] :=
       if: !"v" then
         delete [ #((4 + n * ty.(ty_size))%nat); "v"];;
@@ -133,8 +134,10 @@ Section smallvec_basic.
         delete [ #((4 + n * ty.(ty_size))%nat); "v"];;
         return: [new [ #0]].
 
-  Lemma smallvec_delete_type {𝔄} n (ty: type 𝔄) :
-    typed_val (smallvec_delete n ty) (fn(∅; smallvec n ty) → ()) (λ post _, post ()).
+  (* Rust's SmallVec::drop
+    For simplicity, we skip drop of the elements *)
+  Lemma smallvec_drop_type {𝔄} n (ty: type 𝔄) :
+    typed_val (smallvec_drop n ty) (fn(∅; smallvec n ty) → ()) (λ post _, post ()).
   Proof.
     eapply type_fn; [apply _|]=> _ ??[v[]]. simpl_subst.
     iIntros (?[?[]]?) "_ TIME _ _ _ Na L C [v _] Obs".
@@ -181,6 +184,7 @@ Section smallvec_basic.
       letalloc: "r" <- !("v" +ₗ #2) in
       return: ["r"].
 
+  (* Rust's SmallVec::len *)
   Lemma smallvec_len_type {𝔄} n (ty: type 𝔄) :
     typed_val smallvec_len (fn<α>(∅; &shr{α} (smallvec n ty)) → int)
       (λ post '-[v], post (length v)).

theories/typing/lib/smallvec/smallvec_index.v

@@ -21,6 +21,7 @@ Section smallvec_index.
         delete [ #1; "v"];; delete [ #1; "i"];;
         return: ["r"].
 
+  (* Rust's SmallVec::index *)
   (* The precondition requires that the index is within bounds of the list *)
   Lemma smallvec_index_shr_type {𝔄} n (ty: type 𝔄) :
     typed_val (smallvec_index ty) (fn<α>(∅; &shr{α} (smallvec n ty), int) → &shr{α} ty)
@@ -75,6 +76,7 @@ Section smallvec_index.
         by rewrite Eqi -vlookup_lookup -vapply_lookup=> <-.
   Qed.
 
+  (* Rust's SmallVec::index_mut *)
   (* The precondition requires that the index is within bounds of the list *)
   Lemma smallvec_index_uniq_type {𝔄} n (ty: type 𝔄) :
     typed_val (smallvec_index ty) (fn<α>(∅; &uniq{α} (smallvec n ty), int) → &uniq{α} ty)

theories/typing/lib/smallvec/smallvec_pop.v

@@ -27,6 +27,7 @@ Section smallvec_pop.
           "r" +ₗ #1 <-{ty.(ty_size)} !(!("v'" +ₗ #1) +ₗ "len'" * #ty.(ty_size));;
           return: ["r"].
 
+  (* Rust's SmallVec::pop *)
   Lemma smallvec_pop_type {𝔄} n (ty: type 𝔄) :
     typed_val (smallvec_pop ty) (fn<α>(∅; &uniq{α} (smallvec n ty)) → option_ty ty)
       (λ post '-[(al, al')], al' = removelast al → post (last_error al)).

theories/typing/lib/smallvec/smallvec_push.v

@@ -100,6 +100,7 @@ Section smallvec_push.
       delete [ #ty.(ty_size); "x"];;
       let: "r" := new [ #0] in return: ["r"].
 
+  (* Rust's SmallVec::push *)
   Lemma smallvec_push_type {𝔄} n (ty: type 𝔄) :
     typed_val (smallvec_push n ty) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ())
       (λ post '-[(al, al'); a], al' = al ++ [a] → post ()).

theories/typing/lib/smallvec/smallvec_slice.v

@@ -8,7 +8,7 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section smallvec_slice.
   Context `{!typeG Σ}.
 
-  Definition smallvec_to_slice: val :=
+  Definition smallvec_as_slice: val :=
     fn: ["bv"] :=
       let: "v" := !"bv" in delete [ #1; "bv"];;
       let: "r" := new [ #2] in "r" +ₗ #1 <- !("v" +ₗ #2);;
@@ -17,8 +17,8 @@ Section smallvec_slice.
       else
         "r" <- !("v" +ₗ #1);; return: ["r"].
 
-  Lemma smallvec_to_uniq_slice_type {𝔄} n (ty: type 𝔄) :
-    typed_val smallvec_to_slice (fn<α>(∅; &uniq{α} (smallvec n ty)) → uniq_slice α ty)
+  Lemma smallvec_as_slice_uniq_type {𝔄} n (ty: type 𝔄) :
+    typed_val smallvec_as_slice (fn<α>(∅; &uniq{α} (smallvec n ty)) → uniq_slice α ty)
       (λ post '-[(al, al')], length al' = length al → post (zip al al')).
   Proof.
     eapply type_fn; [apply _|]=>/= α ??[bv[]]. simpl_subst.