From 7612357fcae2376c170ecf643aaa85b29f38a72d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 1 Apr 2022 23:06:08 +0900
Subject: [PATCH] Add comments on corresponding Rust methods and tweak some
names
---
README.md | 108 +++++++++---------
theories/typing/examples/inc_vec.v | 4 +-
theories/typing/lib/cell.v | 8 ++
theories/typing/lib/list.v | 3 +
theories/typing/lib/maybe_uninit.v | 6 +
theories/typing/lib/mutex/mutex.v | 10 +-
theories/typing/lib/mutex/mutexguard.v | 5 +
theories/typing/lib/option.v | 10 +-
theories/typing/lib/panic.v | 2 +
theories/typing/lib/slice/array_slice.v | 7 +-
theories/typing/lib/slice/iter.v | 3 +
theories/typing/lib/slice/slice_basic.v | 1 +
theories/typing/lib/slice/slice_split.v | 3 +-
theories/typing/lib/slice/uniq_slice.v | 1 +
theories/typing/lib/smallvec/smallvec.v | 1 +
theories/typing/lib/smallvec/smallvec_basic.v | 10 +-
theories/typing/lib/smallvec/smallvec_index.v | 2 +
theories/typing/lib/smallvec/smallvec_pop.v | 1 +
theories/typing/lib/smallvec/smallvec_push.v | 1 +
theories/typing/lib/smallvec/smallvec_slice.v | 6 +-
theories/typing/lib/spawn.v | 3 +
theories/typing/lib/swap.v | 1 +
theories/typing/lib/vec/vec.v | 1 +
theories/typing/lib/vec/vec_basic.v | 10 +-
theories/typing/lib/vec/vec_index.v | 2 +
theories/typing/lib/vec/vec_pushpop.v | 2 +
theories/typing/lib/vec/vec_slice.v | 7 +-
27 files changed, 140 insertions(+), 78 deletions(-)
diff --git a/README.md b/README.md
index 9dcd8222..cf222c84 100644
--- a/README.md
+++ b/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.
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index 22a25340..c65eb0c4 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/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 ())).
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 23666066..6f72f4fe 100644
--- a/theories/typing/lib/cell.v
+++ b/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').
diff --git a/theories/typing/lib/list.v b/theories/typing/lib/list.v
index d548af41..cd496e63 100644
--- a/theories/typing/lib/list.v
+++ b/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.
diff --git a/theories/typing/lib/maybe_uninit.v b/theories/typing/lib/maybe_uninit.v
index ed942960..e51e18a3 100644
--- a/theories/typing/lib/maybe_uninit.v
+++ b/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)
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 66ebcb7d..146ffcdd 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/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.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index ff880906..3f225436 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/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 ()).
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index a00aa0ce..9880b64e 100644
--- a/theories/typing/lib/option.v
+++ b/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).
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 4a21134d..ae437158 100644
--- a/theories/typing/lib/panic.v
+++ b/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).
diff --git a/theories/typing/lib/slice/array_slice.v b/theories/typing/lib/slice/array_slice.v
index 4d001b6a..0529ef1a 100644
--- a/theories/typing/lib/slice/array_slice.v
+++ b/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.
diff --git a/theories/typing/lib/slice/iter.v b/theories/typing/lib/slice/iter.v
index 217a4990..42c8ef13 100644
--- a/theories/typing/lib/slice/iter.v
+++ b/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))
diff --git a/theories/typing/lib/slice/slice_basic.v b/theories/typing/lib/slice/slice_basic.v
index 81ad3658..4e8d5f1a 100644
--- a/theories/typing/lib/slice/slice_basic.v
+++ b/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)).
diff --git a/theories/typing/lib/slice/slice_split.v b/theories/typing/lib/slice/slice_split.v
index 2205c900..3e91d84b 100644
--- a/theories/typing/lib/slice/slice_split.v
+++ b/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],
diff --git a/theories/typing/lib/slice/uniq_slice.v b/theories/typing/lib/slice/uniq_slice.v
index 6fffd2ad..75038913 100644
--- a/theories/typing/lib/slice/uniq_slice.v
+++ b/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) ∗
diff --git a/theories/typing/lib/smallvec/smallvec.v b/theories/typing/lib/smallvec/smallvec.v
index 520748e5..31d09ccb 100644
--- a/theories/typing/lib/smallvec/smallvec.v
+++ b/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);
diff --git a/theories/typing/lib/smallvec/smallvec_basic.v b/theories/typing/lib/smallvec/smallvec_basic.v
index 08fce156..e1f09116 100644
--- a/theories/typing/lib/smallvec/smallvec_basic.v
+++ b/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)).
diff --git a/theories/typing/lib/smallvec/smallvec_index.v b/theories/typing/lib/smallvec/smallvec_index.v
index 216d4033..9c49ecb1 100644
--- a/theories/typing/lib/smallvec/smallvec_index.v
+++ b/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)
diff --git a/theories/typing/lib/smallvec/smallvec_pop.v b/theories/typing/lib/smallvec/smallvec_pop.v
index a5c1c4e8..fe118ba4 100644
--- a/theories/typing/lib/smallvec/smallvec_pop.v
+++ b/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)).
diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index 06f1a12d..54414306 100644
--- a/theories/typing/lib/smallvec/smallvec_push.v
+++ b/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 ()).
diff --git a/theories/typing/lib/smallvec/smallvec_slice.v b/theories/typing/lib/smallvec/smallvec_slice.v
index f27c7dc4..b392e8dc 100644
--- a/theories/typing/lib/smallvec/smallvec_slice.v
+++ b/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.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index eec53aeb..56e6ad5a 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -14,6 +14,7 @@ Section spawn.
Definition join_future {𝔄} (ty: type 𝔄) (Φ: pred' 𝔄) (v: val) : iProp Σ :=
∀tid, ∃vπ d, ⟨π, Φ (vπ π)⟩ ∗ ⧖d ∗ (box ty).(ty_own) vπ d tid [v].
+ (* Rust's thread::JoinHandle<T> *)
Program Definition join_handle {𝔄} (ty: type 𝔄) : type (predₛ 𝔄) := {|
ty_size := 1; ty_lfts := ty.(ty_lfts); ty_E := ty.(ty_E);
ty_own Φπ _ _ vl := [loc[l] := vl] ∃Φ, ⌜Φπ = const Φ⌝ ∗
@@ -102,6 +103,7 @@ Section spawn.
letalloc: "r" <- "j" in
return: ["r"].
+ (* Rust's thread::spawn *)
Lemma spawn_type {𝔄 𝔅} (Φ: pred' 𝔅) tr (fty: type 𝔄) (retty: type 𝔅)
call_once `{!Send fty, !Send retty} :
typed_val call_once (fn(∅; fty) → retty) tr →
@@ -142,6 +144,7 @@ Section spawn.
let: "r" := spawn.join ["j"] in
return: ["r"].
+ (* Rust's JoinHandle::join *)
Lemma join_type {𝔄} (retty: type 𝔄) :
typed_val join (fn(∅; join_handle retty) → retty)
(λ post '-[Φ], ∀a: 𝔄, Φ a → post a).
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index c7e35b05..253fc315 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -14,6 +14,7 @@ Section swap.
let: "r" := new [ #0] in
return: ["r"].
+ (* Rust's mem::swap *)
Lemma swap_type {𝔄} (ty: type 𝔄) :
typed_val (swap ty) (fn<α>(∅; &uniq{α} ty, &uniq{α} ty) → ())
(λ post '-[(a, a'); (b, b')], a' = b → b' = a → post ()).
diff --git a/theories/typing/lib/vec/vec.v b/theories/typing/lib/vec/vec.v
index d6f1a65a..a768d99f 100644
--- a/theories/typing/lib/vec/vec.v
+++ b/theories/typing/lib/vec/vec.v
@@ -21,6 +21,7 @@ Section vec.
iExists [_;_;_]. iFrame "↦". iExists _, _, _, _. by iFrame.
Qed.
+ (* Rust's Vec<T> *)
Program Definition vec_ty {𝔄} (ty: type 𝔄) : type (listₛ 𝔄) := {|
ty_size := 3; ty_lfts := ty.(ty_lfts); ty_E := ty.(ty_E);
ty_own alπ d tid vl :=
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index 29b2742f..b405b638 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -76,6 +76,7 @@ Section vec_basic.
eqtype E L ty ty' f g → eqtype E L (vec_ty ty) (vec_ty ty') (map f) (map g).
Proof. move=> [??]. split; by apply vec_subtype. Qed.
+ (* Rust's Vec::new *)
Definition vec_new: val :=
fn: [] :=
let: "r" := new [ #3] in
@@ -103,14 +104,16 @@ Section vec_basic.
iSplit; [by iNext|]. iExists []. by rewrite heap_mapsto_vec_nil.
Qed.
- Definition vec_delete {𝔄} (ty: type 𝔄) : val :=
+ Definition vec_drop {𝔄} (ty: type 𝔄) : val :=
fn: ["v"] :=
delete [(!("v" +ₗ #1) + !("v" +ₗ #2)) * #ty.(ty_size); !"v"];;
delete [ #3; "v"];;
return: [new [ #0]].
- Lemma vec_delete_type {𝔄} (ty: type 𝔄) :
- typed_val (vec_delete ty) (fn(∅; vec_ty ty) → ()) (λ post _, post ()).
+ (* Rust's Vec::drop
+ For simplicity, we skip drop of the elements *)
+ Lemma vec_drop_type {𝔄} (ty: type 𝔄) :
+ typed_val (vec_drop ty) (fn(∅; vec_ty ty) → ()) (λ post _, post ()).
Proof.
eapply type_fn; [apply _|]=> _ ??[v[]]. simpl_subst.
iIntros (?[?[]]?) "_ TIME _ _ _ Na L C [v _] Obs".
@@ -144,6 +147,7 @@ Section vec_basic.
letalloc: "r" <- !("v" +ₗ #1) in
return: ["r"].
+ (* Rust's Vec::len *)
Lemma vec_len_type {𝔄} (ty: type 𝔄) :
typed_val vec_len (fn<α>(∅; &shr{α} (vec_ty ty)) → int)
(λ post '-[v], post (length v)).
diff --git a/theories/typing/lib/vec/vec_index.v b/theories/typing/lib/vec/vec_index.v
index 50bc0b8b..e1294ecf 100644
--- a/theories/typing/lib/vec/vec_index.v
+++ b/theories/typing/lib/vec/vec_index.v
@@ -15,6 +15,7 @@ Section vec_index.
delete [ #1; "v"];; delete [ #1; "i"];;
return: ["r"].
+ (* Rust's Vec::index *)
(* The precondition requires that the index is within bounds of the list *)
Lemma vec_index_shr_type {𝔄} (ty: type 𝔄) :
typed_val (vec_index ty) (fn<α>(∅; &shr{α} (vec_ty ty), int) → &shr{α} ty)
@@ -52,6 +53,7 @@ Section vec_index.
by rewrite Eqi -vlookup_lookup -vapply_lookup=> <-.
Qed.
+ (* Rust's Vec::index_mut *)
(* The precondition requires that the index is within bounds of the list *)
Lemma vec_index_uniq_type {𝔄} (ty: type 𝔄) :
typed_val (vec_index ty) (fn<α>(∅; &uniq{α} (vec_ty ty), int) → &uniq{α} ty)
diff --git a/theories/typing/lib/vec/vec_pushpop.v b/theories/typing/lib/vec/vec_pushpop.v
index 089992a7..fe455138 100644
--- a/theories/typing/lib/vec/vec_pushpop.v
+++ b/theories/typing/lib/vec/vec_pushpop.v
@@ -15,6 +15,7 @@ Section vec_pushpop.
vec_push_core ty ["v'"; "x"];; delete [ #ty.(ty_size); "x"];;
let: "r" := new [ #0] in return: ["r"].
+ (* Rust's Vec::push *)
Lemma vec_push_type {𝔄} (ty: type 𝔄) :
typed_val (vec_push ty) (fn<α>(∅; &uniq{α} (vec_ty ty), ty) → ())
(λ post '-[(al, al'); a], al' = al ++ [a] → post ()).
@@ -73,6 +74,7 @@ Section vec_pushpop.
"r" <- #1;; "r" +ₗ #1 <-{ty.(ty_size)} ! (!"v'" +ₗ "len'" * #ty.(ty_size));;
return: ["r"].
+ (* Rust's Vec::pop *)
Lemma vec_pop_type {𝔄} (ty: type 𝔄) :
typed_val (vec_pop ty) (fn<α>(∅; &uniq{α} (vec_ty ty)) → option_ty ty)
(λ post '-[(al, al')], al' = removelast al → post (last_error al)).
diff --git a/theories/typing/lib/vec/vec_slice.v b/theories/typing/lib/vec/vec_slice.v
index 337f9c30..d19b8bdc 100644
--- a/theories/typing/lib/vec/vec_slice.v
+++ b/theories/typing/lib/vec/vec_slice.v
@@ -8,15 +8,16 @@ Implicit Type 𝔄 𝔅: syn_type.
Section vec_slice.
Context `{!typeG Σ}.
- Definition vec_to_slice: val :=
+ Definition vec_as_slice: val :=
fn: ["bv"] :=
let: "v" := !"bv" in delete [ #1; "bv"];;
let: "r" := new [ #2] in
"r" <- !"v";; "r" +ₗ #1 <- !("v" +ₗ #1);;
return: ["r"].
- Lemma vec_to_uniq_slice_type {𝔄} (ty: type 𝔄) :
- typed_val vec_to_slice (fn<α>(∅; &uniq{α} (vec_ty ty)) → uniq_slice α ty)
+ (* Rust's Vec::as_slice_mut *)
+ Lemma vec_as_slice_uniq_type {𝔄} (ty: type 𝔄) :
+ typed_val vec_as_slice (fn<α>(∅; &uniq{α} (vec_ty ty)) → uniq_slice α ty)
(λ post '-[(al, al')], length al' = length al → post (zip al al')).
Proof.
eapply type_fn; [apply _|]=>/= α ??[bv[]]. simpl_subst.
--
GitLab