Adapt to finite sets and maps

verified-node-replication/rust-toolchain.toml

@@ -1,2 +1,2 @@
 [toolchain]
-channel = "1.76.0"
+channel = "1.96.0"

verified-node-replication/src/exec/rwlock.rs

@@ -69,7 +69,7 @@ struct_with_invariants!{
         ref_counts: Vec<CachePadded<AtomicU64<_, RwLockSpec::ref_counts<PointsTo<T>>, _>>>,
         /// the spec instance
         inst: Tracked<RwLockSpec::Instance<PointsTo<T>>>,
-        user_inv: Ghost<Set<T>>,
+        user_inv: Ghost<ISet<T>>,
     }
 
     pub closed spec fn wf(&self) -> bool {
@@ -147,8 +147,8 @@ impl<T> RwLock<T> {
         // create the pcell object
         let (pcell_data, Tracked(mut pcell_token)) = PCell::new(t);
         // create the set of allowed data structures
-        let ghost set_inv = Set::new(inv@);
-        let ghost user_inv = Set::new(
+        let ghost set_inv = ISet::new(inv@);
+        let ghost user_inv = ISet::new(
             |s: PointsTo<T>|
                 {
                     &&& equal(s@.pcell, pcell_data.id())
@@ -157,10 +157,10 @@ impl<T> RwLock<T> {
                 },
         );
         proof {
-            // user_inv: Set<T>, t: T
+            // user_inv: ISet<T>, t: T
             // initialize_full(user_inv, perm@, Option::Some(perm.get()));
             //
-            // initialize(rc_width: int, init_t: T, user_inv: Set<T>,) {
+            // initialize(rc_width: int, init_t: T, user_inv: ISet<T>,) {
             let tracked (
                 Tracked(inst0),
                 Tracked(exc_locked_token0),

verified-node-replication/src/spec/cyclicbuffer.rs

@@ -349,14 +349,14 @@ tokenized_state_machine! { CyclicBuffer<DT: Dispatch> {
             init num_replicas = num_replicas;
             init head = 0;
             init tail = 0;
-            init local_versions = Map::new(|i: NodeId| 0 <= i < num_replicas, |i: NodeId| 0);
+            init local_versions = Map::new(Set::range(0, num_replicas), |i: NodeId| 0);
 
             require(forall |i: int| (-buffer_size <= i < 0 <==> contents.contains_key(i)));
             require(forall |i: int| #[trigger] contents.contains_key(i) ==> stored_type_inv(contents[i], i, cell_ids[log_entry_idx(i, buffer_size) as int], unbounded_log_instance));
             init contents = contents;
 
-            init alive_bits = Map::new(|i: nat| 0 <= i < buffer_size, |i: nat| !log_entry_alive_value(i as int, buffer_size));
-            init combiner = Map::new(|i: NodeId| 0 <= i < num_replicas, |i: NodeId| CombinerState::Idle);
+            init alive_bits = Map::new(Set::range(0, buffer_size), |i: nat| !log_entry_alive_value(i as int, buffer_size));
+            init combiner = Map::new(Set::range(0, num_replicas), |i: NodeId| CombinerState::Idle);
         }
     }
 
@@ -541,7 +541,7 @@ tokenized_state_machine! { CyclicBuffer<DT: Dispatch> {
 
             // construct the entries in the log we withdraw
             birds_eye let withdrawn = Map::new(
-                |i: int| pre.tail - pre.buffer_size <= i < new_tail - pre.buffer_size,
+                Set::range(pre.tail - pre.buffer_size, new_tail - pre.buffer_size),
                 |i: int| pre.contents[i],
             );
 

verified-node-replication/src/spec/flat_combiner.rs

@@ -185,8 +185,8 @@ FlatCombiner {
         initialize(num_threads: nat) {
             init num_threads = num_threads;
 
-            init clients = Map::new(|i:ThreadId| i < num_threads, |i| ClientState::Idle);
-            init slots = Map::new(|i: ThreadId| i < num_threads, |i| SlotState::Empty);
+            init clients = Map::new(Set::range(0, num_threads), |i| ClientState::Idle);
+            init slots = Map::new(Set::range(0, num_threads), |i| SlotState::Empty);
 
             init combiner = CombinerState::Collecting(Seq::empty());
         }

verified-node-replication/src/spec/rwlock.rs

@@ -14,7 +14,7 @@ tokenized_state_machine!{
     RwLockSpec<T> {
         fields {
             #[sharding(constant)]
-            pub user_inv: Set<T>,
+            pub user_inv: ISet<T>,
 
             #[sharding(constant)]
             pub rc_width: int,
@@ -42,15 +42,15 @@ tokenized_state_machine!{
         }
 
         init!{
-            initialize(rc_width: int, init_t: T, user_inv: Set<T>,) {
+            initialize(rc_width: int, init_t: T, user_inv: ISet<T>,) {
                 require(0 < rc_width);
                 require(user_inv.contains(init_t));
                 init rc_width = rc_width;
                 init user_inv = user_inv;
                 init storage = Option::Some(init_t);
                 init exc_locked = false;
                 init ref_counts = Map::new(
-                    |i| 0 <= i < rc_width,
+                    Set::range(0, rc_width),
                     |i| 0,
                 );
                 init exc_pending = Option::None;
@@ -218,7 +218,7 @@ tokenized_state_machine!{
         }
 
         #[inductive(initialize)]
-        fn initialize_inductive(post: Self, rc_width: int, init_t: T,  user_inv: Set<T>) {
+        fn initialize_inductive(post: Self, rc_width: int, init_t: T,  user_inv: ISet<T>) {
             assert forall |r| 0 <= r < post.rc_width implies
                 #[trigger] post.ref_counts.index(r) ==
                     post.shared_pending.count(r) as int +

verified-node-replication/src/spec/unbounded_log.rs

@@ -583,12 +583,12 @@ UnboundedLog<DT: Dispatch> {
             init num_replicas = number_of_nodes;
             init log = Map::empty();
             init tail = 0;
-            init replicas = Map::new(|n: NodeId| n < number_of_nodes, |n| DT::init_spec());
-            init local_versions = Map::new(|n: NodeId| n < number_of_nodes, |n| 0);
+            init replicas = Map::new(Set::range(0, number_of_nodes), |n| DT::init_spec());
+            init local_versions = Map::new(Set::range(0, number_of_nodes), |n| 0);
             init version_upper_bound = 0;
             init local_reads = Map::empty();
             init local_updates = Map::empty();
-            init combiner = Map::new(|n: NodeId| n < number_of_nodes, |n| CombinerState::Ready);
+            init combiner = Map::new(Set::range(0, number_of_nodes), |n| CombinerState::Ready);
         }
     }
 
@@ -1286,9 +1286,6 @@ pub proof fn combiner_request_ids_finite(combiners: Map<NodeId, CombinerState>)
         assert(combiner_request_ids(combiners.remove(node_id)).finite()) by {
             combiner_request_ids_finite(combiners.remove(node_id));
         }
-        assert(seq_to_set(combiners[node_id].queued_ops()).finite()) by {
-            seq_to_set_is_finite(combiners[node_id].queued_ops());
-        }
     }
 }
 

verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs

@@ -180,7 +180,7 @@ spec fn interp_readonly_reqs<DT: Dispatch>(local_reads: Map<nat, ReadonlyState<D
     SReadReq<DT::ReadOperation>,
 > {
     Map::new(
-        |rid| local_reads.contains_key(rid),
+        local_reads.dom(),
         |rid|
             match local_reads.index(rid) {
                 ReadonlyState::Init { op } => SReadReq::Init { op },
@@ -205,7 +205,7 @@ spec fn interp_update_reqs<DT: Dispatch>(local_updates: Map<LogIdx, UpdateState<
     DT::WriteOperation,
 > {
     Map::new(
-        |rid| local_updates.contains_key(rid) && local_updates.index(rid).is_Init(),
+        local_updates.dom().filter(|rid| local_updates.index(rid).is_Init()),
         |rid|
             match local_updates.index(rid) {
                 UpdateState::Init { op } => op,
@@ -219,7 +219,7 @@ spec fn interp_update_resps<DT: Dispatch>(local_updates: Map<nat, UpdateState<DT
     SUpdateResp,
 > {
     Map::new(
-        |rid| local_updates.contains_key(rid) && !local_updates.index(rid).is_Init(),
+        local_updates.dom().filter(|rid| !local_updates.index(rid).is_Init()),
         |rid|
             match local_updates.index(rid) {
                 UpdateState::Init { op } => arbitrary(),

verified-node-replication/src/spec/utils.rs

@@ -98,17 +98,7 @@ proof fn seq_to_set_equal_rec<A>(seq: Seq<A>)
 }
 
 pub open spec fn seq_to_set<A>(seq: Seq<A>) -> Set<A> {
-    Set::new(|a: A| seq.contains(a))
-}
-
-pub proof fn seq_to_set_is_finite<A>(seq: Seq<A>)
-    ensures
-        seq_to_set(seq).finite(),
-{
-    assert(seq_to_set(seq).finite()) by {
-        seq_to_set_equal_rec(seq);
-        seq_to_set_rec_is_finite(seq);
-    }
+    seq.to_set()
 }
 
 pub open spec fn map_new_rec<V>(dom: nat, val: V) -> Map<nat, V>