diff --git a/verified-node-replication/rust-toolchain.toml b/verified-node-replication/rust-toolchain.toml index 624eb0e..0f87b44 100644 --- a/verified-node-replication/rust-toolchain.toml +++ b/verified-node-replication/rust-toolchain.toml @@ -1,2 +1,2 @@ [toolchain] -channel = "1.76.0" +channel = "1.96.0" diff --git a/verified-node-replication/src/exec/rwlock.rs b/verified-node-replication/src/exec/rwlock.rs index a2b52a8..b90f631 100644 --- a/verified-node-replication/src/exec/rwlock.rs +++ b/verified-node-replication/src/exec/rwlock.rs @@ -69,7 +69,7 @@ struct_with_invariants!{ ref_counts: Vec>, _>>>, /// the spec instance inst: Tracked>>, - user_inv: Ghost>, + user_inv: Ghost>, } pub closed spec fn wf(&self) -> bool { @@ -147,8 +147,8 @@ impl RwLock { // 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| { &&& equal(s@.pcell, pcell_data.id()) @@ -157,10 +157,10 @@ impl RwLock { }, ); proof { - // user_inv: Set, t: T + // user_inv: ISet, t: T // initialize_full(user_inv, perm@, Option::Some(perm.get())); // - // initialize(rc_width: int, init_t: T, user_inv: Set,) { + // initialize(rc_width: int, init_t: T, user_inv: ISet,) { let tracked ( Tracked(inst0), Tracked(exc_locked_token0), diff --git a/verified-node-replication/src/spec/cyclicbuffer.rs b/verified-node-replication/src/spec/cyclicbuffer.rs index d44b692..fea9189 100644 --- a/verified-node-replication/src/spec/cyclicbuffer.rs +++ b/verified-node-replication/src/spec/cyclicbuffer.rs @@ -349,14 +349,14 @@ tokenized_state_machine! { CyclicBuffer { 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 { // 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], ); diff --git a/verified-node-replication/src/spec/flat_combiner.rs b/verified-node-replication/src/spec/flat_combiner.rs index 6938aec..afecd02 100644 --- a/verified-node-replication/src/spec/flat_combiner.rs +++ b/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()); } diff --git a/verified-node-replication/src/spec/rwlock.rs b/verified-node-replication/src/spec/rwlock.rs index 22ba2c6..b6ed287 100644 --- a/verified-node-replication/src/spec/rwlock.rs +++ b/verified-node-replication/src/spec/rwlock.rs @@ -14,7 +14,7 @@ tokenized_state_machine!{ RwLockSpec { fields { #[sharding(constant)] - pub user_inv: Set, + pub user_inv: ISet, #[sharding(constant)] pub rc_width: int, @@ -42,7 +42,7 @@ tokenized_state_machine!{ } init!{ - initialize(rc_width: int, init_t: T, user_inv: Set,) { + initialize(rc_width: int, init_t: T, user_inv: ISet,) { require(0 < rc_width); require(user_inv.contains(init_t)); init rc_width = rc_width; @@ -50,7 +50,7 @@ tokenized_state_machine!{ 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) { + fn initialize_inductive(post: Self, rc_width: int, init_t: T, user_inv: ISet) { assert forall |r| 0 <= r < post.rc_width implies #[trigger] post.ref_counts.index(r) == post.shared_pending.count(r) as int + diff --git a/verified-node-replication/src/spec/unbounded_log.rs b/verified-node-replication/src/spec/unbounded_log.rs index bb6de98..3d24b82 100644 --- a/verified-node-replication/src/spec/unbounded_log.rs +++ b/verified-node-replication/src/spec/unbounded_log.rs @@ -583,12 +583,12 @@ UnboundedLog { 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) 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()); - } } } diff --git a/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs b/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs index 483a240..4e6d0f4 100644 --- a/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs +++ b/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs @@ -180,7 +180,7 @@ spec fn interp_readonly_reqs(local_reads: Map, > { 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(local_updates: Map { 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(local_updates: Map { 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(), diff --git a/verified-node-replication/src/spec/utils.rs b/verified-node-replication/src/spec/utils.rs index 73e1511..e2c3a13 100644 --- a/verified-node-replication/src/spec/utils.rs +++ b/verified-node-replication/src/spec/utils.rs @@ -98,17 +98,7 @@ proof fn seq_to_set_equal_rec(seq: Seq) } pub open spec fn seq_to_set(seq: Seq) -> Set { - Set::new(|a: A| seq.contains(a)) -} - -pub proof fn seq_to_set_is_finite(seq: Seq) - 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(dom: nat, val: V) -> Map