Change some struct mode

Author: rikosellic

…extra/src/resource/ghost_resource/sum.rs …xtra/src/resource/ghost_resource/csum.rsvstd_extra/src/resource/ghost_resource/sum.rs renamed to vstd_extra/src/resource/ghost_resource/csum.rs vstd_extra/src/resource/ghost_resource/sum.rs renamed to vstd_extra/src/resource/ghost_resource/csum.rs

@@ -1,5 +1,5 @@
 //！ Ghost resources availbe for use in proofs, based on previous resource algebras.
 pub mod excl;
 pub mod frac;
-pub mod sum;
+pub mod csum;
 pub mod tokens;

vstd_extra/src/resource/ghost_resource/mod.rs

@@ -11,7 +11,7 @@ verus! {
 ///
 /// In modern Iris, it uses CMRA instead of PCM, which uses a core for every element instead of a unit element.
 /// Here we add a unit element to stick to the PCM definition.
-pub tracked enum AgreeR<A> {
+pub ghost enum AgreeR<A> {
     Unit,
     /// Agreement on a value.
     Agree(A),

vstd_extra/src/resource/pcm/agree.rs

@@ -1,4 +1,4 @@
-//! Csum resource algebra
+//! Csum resource algebra.
 //!
 //! For Iris definition, see:
 //! <https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/csum.v>
@@ -11,7 +11,7 @@ verus! {
 ///
 /// In modern Iris, it uses CMRA instead of PCM, which uses a core for every element instead of a unit element.
 /// Here we add a unit element to stick to the PCM definition.
-pub tracked enum CsumR<A, B> {
+pub ghost enum CsumR<A, B> {
     Unit,
     Cinl(A),
     Cinr(B),

vstd_extra/src/resource/pcm/csum.rs

@@ -15,7 +15,7 @@ verus! {
 
 /// Fractional PCM
 #[verifier::ext_equal]
-pub tracked enum FracR<T> {
+pub ghost enum FracR<T> {
     Unit,
     Frac(real, T),
     Invalid,

vstd_extra/src/resource/pcm/frac.rs

@@ -0,0 +1,21 @@
+//! Csum storage protocol.
+
+use vstd::prelude::*;
+use vstd::pcm::Loc;
+use vstd::prelude::*;
+use vstd::storage_protocol::*;
+use crate::sum::*;
+
+verus!{
+
+/// The Csum storage protocol.
+pub ghost enum CsumP<A, B> {
+    Unit,
+    Cinl(A),
+    Cinr(B),
+    CsumInvalid,
+}
+
+
+
+}

vstd_extra/src/resource/storage_protocol/csum.rs

@@ -10,7 +10,7 @@ broadcast use group_map_axioms;
 
 /// The fractional protocol monoid.
 #[verifier::ext_equal]
-pub tracked enum FracP<T> {
+pub ghost enum FracP<T> {
     Unit,
     Frac(real, T),
     Invalid,

vstd_extra/src/resource/storage_protocol/frac.rs

@@ -7,7 +7,7 @@ use vstd::storage_protocol::*;
 verus! {
 
 /// The hybrid product of a PCM and a storage-protocol resource algebra.
-pub tracked struct HybridProduct<P: PCM, S: Protocol<K, V>, K, V> {
+pub ghost struct HybridProduct<P: PCM, S: Protocol<K, V>, K, V> {
     pub pcm: P,
     pub protocol: S,
     /// A Rust compiler restriction.

vstd_extra/src/resource/storage_protocol/hybrid_product.rs

@@ -1,3 +1,4 @@
 //！ Definition of the Leaf-style storage protocol resource algebra.
+pub mod csum;
 pub mod frac;
 pub mod hybrid_product;