Skip to content

Commit 7d8e82c

Browse files
bsdinisbsdinis
authored
resource: replicate Map/Set changes in GhostMap/GhostSet (#2551)
1 parent 4ea7d0f commit 7d8e82c

17 files changed

Lines changed: 2797 additions & 187 deletions

File tree

source/vstd/resource/agree.rs renamed to source/vstd/resource/combinators/agree.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
use super::super::prelude::*;
2-
use super::algebra::Resource;
3-
use super::algebra::ResourceAlgebra;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::Resource;
3+
use super::super::algebra::ResourceAlgebra;
44

55
verus! {
66

source/vstd/resource/auth.rs renamed to source/vstd/resource/combinators/auth.rs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
use super::super::prelude::*;
2-
use super::algebra::ResourceAlgebra;
3-
use super::exclusive::ExclusiveRA;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::ResourceAlgebra;
3+
use super::super::exclusive::ExclusiveRA;
44
#[cfg(verus_keep_ghost)]
5-
use super::option::lemma_incl_opt_rev;
6-
use super::pcm::PCM;
5+
use super::super::option::lemma_incl_opt_rev;
6+
use super::super::pcm::PCM;
77
#[cfg(verus_keep_ghost)]
8-
use super::relations::incl;
8+
use super::super::relations::incl;
99
#[cfg(verus_keep_ghost)]
10-
use super::relations::lemma_incl_transitive;
10+
use super::super::relations::lemma_incl_transitive;
1111

1212
verus! {
1313

source/vstd/resource/exclusive.rs renamed to source/vstd/resource/combinators/exclusive.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
use super::super::prelude::*;
2-
use super::algebra::ResourceAlgebra;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::ResourceAlgebra;
33

44
verus! {
55

source/vstd/resource/frac.rs renamed to source/vstd/resource/combinators/frac.rs

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
use super::super::modes::*;
2-
use super::super::prelude::*;
3-
use super::Loc;
4-
use super::agree::AgreementRA;
5-
use super::algebra::Resource;
6-
use super::algebra::ResourceAlgebra;
7-
use super::pcm::PCM;
8-
use super::product::ProductRA;
9-
use super::storage_protocol::*;
10-
use super::*;
1+
use super::super::super::modes::*;
2+
use super::super::super::prelude::*;
3+
use super::super::Loc;
4+
use super::super::agree::AgreementRA;
5+
use super::super::algebra::Resource;
6+
use super::super::algebra::ResourceAlgebra;
7+
use super::super::pcm::PCM;
8+
use super::super::product::ProductRA;
9+
use super::super::storage_protocol::*;
10+
use super::super::*;
1111

1212
verus! {
1313

@@ -93,7 +93,7 @@ type FractionalCarrier<T> = ProductRA<FractionRA, AgreementRA<T>>;
9393
/// An implementation of a resource for fractional ownership of a ghost variable.
9494
///
9595
/// If you just want to split the permission in half, you can also use the
96-
/// [`GhostVar<T>`](super::ghost_var::GhostVar) and [`GhostVarAuth<T>`](super::ghost_var::GhostVarAuth) library.
96+
/// [`GhostVar<T>`](super::super::ghost_var::GhostVar) and [`GhostVarAuth<T>`](super::super::ghost_var::GhostVarAuth) library.
9797
///
9898
/// ### Example
9999
///

‎source/vstd/resource/combinators/mod.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
pub mod agree;
2+
pub mod auth;
3+
pub mod exclusive;
4+
pub mod frac;
5+
pub mod option;
6+
pub mod product;
7+
pub mod sum;

source/vstd/resource/option.rs renamed to source/vstd/resource/combinators/option.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
use super::super::prelude::*;
2-
use super::algebra::ResourceAlgebra;
3-
use super::pcm::PCM;
4-
use super::relations::*;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::ResourceAlgebra;
3+
use super::super::pcm::PCM;
4+
use super::super::relations::*;
55

66
verus! {
77

@@ -90,7 +90,7 @@ pub proof fn lemma_set_op_opt<RA: ResourceAlgebra>(s: ISet<RA>, t: RA)
9090
ensures
9191
set_op(s, t).map(|b| Some(b)) == set_op(s.map(|x| Some(x)), Some(t)),
9292
{
93-
broadcast use super::super::iset::group_iset_lemmas;
93+
broadcast use super::super::super::iset::group_iset_lemmas;
9494

9595
let s_mapped = s.map(|x| Some(x));
9696
let original = set_op(s, t);

source/vstd/resource/product.rs renamed to source/vstd/resource/combinators/product.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
use super::super::prelude::*;
2-
use super::algebra::ResourceAlgebra;
3-
use super::pcm::PCM;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::ResourceAlgebra;
3+
use super::super::pcm::PCM;
44

55
verus! {
66

source/vstd/resource/sum.rs renamed to source/vstd/resource/combinators/sum.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
use super::super::prelude::*;
2-
use super::algebra::ResourceAlgebra;
1+
use super::super::super::prelude::*;
2+
use super::super::algebra::ResourceAlgebra;
33

44
verus! {
55

source/vstd/resource/frac_opt.rs renamed to source/vstd/resource/impls/frac_opt.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
use super::super::modes::*;
2-
use super::super::prelude::*;
3-
use super::Loc;
4-
use super::storage_protocol::*;
1+
use super::super::super::modes::*;
2+
use super::super::super::prelude::*;
3+
use super::super::Loc;
4+
use super::super::storage_protocol::*;
55

66
verus! {
77

88
broadcast use {
9-
super::super::imap::group_imap_lemmas,
10-
super::super::iset::group_iset_lemmas,
11-
super::super::map::group_map_lemmas,
12-
super::super::set::group_set_lemmas,
9+
super::super::super::imap::group_imap_lemmas,
10+
super::super::super::iset::group_iset_lemmas,
11+
super::super::super::map::group_map_lemmas,
12+
super::super::super::set::group_set_lemmas,
1313
};
1414

1515
/////// Fractional tokens that allow borrowing of resources

source/vstd/resource/ghost_var.rs renamed to source/vstd/resource/impls/ghost_var.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
#[cfg(verus_keep_ghost)]
2-
use super::super::modes::tracked_swap;
3-
use super::super::prelude::*;
4-
use super::Loc;
5-
use super::frac::FracGhost;
2+
use super::super::super::modes::tracked_swap;
3+
use super::super::super::prelude::*;
4+
use super::super::Loc;
5+
use super::super::frac::FracGhost;
66

77
verus! {
88

0 commit comments

Comments
 (0)