diff --git a/verified-node-replication/src/exec/context.rs b/verified-node-replication/src/exec/context.rs index ddcf781..5f4ed87 100644 --- a/verified-node-replication/src/exec/context.rs +++ b/verified-node-replication/src/exec/context.rs @@ -444,38 +444,38 @@ pub open spec fn inv(&self, v: u64, tid: nat, cell: PCell>, &&& (v == 1 ==> self.slots.value().is_Request() || self.slots.value().is_InProgress()) &&& (self.slots.value().is_Empty() ==> { - &&& self.update.is_None() - &&& self.batch_perms.is_None() + &&& self.update.is_none() + &&& self.batch_perms.is_none() }) &&& (self.slots.value().is_Request() ==> { - &&& self.update.is_Some() - &&& self.update.get_Some_0().value().is_Init() - &&& self.update.get_Some_0().key() == self.slots.value().get_ReqId() - &&& self.update.get_Some_0().instance_id() == inst.id() - - &&& self.batch_perms.is_Some() - &&& self.batch_perms.get_Some_0().mem_contents().is_init() - &&& self.batch_perms.get_Some_0()@.pcell == cell.id() - &&& self.batch_perms.get_Some_0().mem_contents().value().op == self.update.get_Some_0().value().get_Init_op() + &&& self.update matches Some(update) + &&& update.value().is_Init() + &&& update.key() == self.slots.value().get_ReqId() + &&& update.instance_id() == inst.id() + + &&& self.batch_perms matches Some(batch_perms) + &&& batch_perms.mem_contents().is_init() + &&& batch_perms@.pcell == cell.id() + &&& batch_perms.mem_contents().value().op == update.value().get_Init_op() }) &&& (self.slots.value().is_InProgress() ==> { - &&& self.update.is_None() - &&& self.batch_perms.is_None() + &&& self.update.is_none() + &&& self.batch_perms.is_none() }) &&& (self.slots.value().is_Response() ==> { - &&& self.update.is_Some() - &&& self.update.get_Some_0().value().is_Done() - &&& self.update.get_Some_0().key() == self.slots.value().get_ReqId() - &&& self.update.get_Some_0().instance_id() == inst.id() - - &&& self.batch_perms.is_Some() - &&& self.batch_perms.get_Some_0().mem_contents().is_init() - &&& self.batch_perms.get_Some_0()@.pcell == cell.id() - &&& self.batch_perms.get_Some_0().mem_contents().value().resp.is_Some() - &&& self.batch_perms.get_Some_0().mem_contents().value().resp.get_Some_0() == self.update.get_Some_0().value().get_Done_ret() + &&& self.update matches Some(update) + &&& update.value().is_Done() + &&& update.key() == self.slots.value().get_ReqId() + &&& update.instance_id() == inst.id() + + &&& self.batch_perms matches Some(batch_perms) + &&& batch_perms.mem_contents().is_init() + &&& batch_perms@.pcell == cell.id() + &&& batch_perms.mem_contents().value().resp matches Some(resp) + &&& resp == update.value().get_Done_ret() }) } } @@ -499,14 +499,14 @@ impl FCClientRequestResponseGhost
{ fc_inst: FlatCombiner::Instance, inst: UnboundedLog::Instance
, ) -> bool { - &&& self.local_updates.is_Some() - &&& self.local_updates.get_Some_0().instance_id() == inst.id() - &&& self.local_updates.get_Some_0().value().is_Init() - &&& self.local_updates.get_Some_0().value().get_Init_op() == op - &&& self.batch_perms.is_Some() - &&& self.batch_perms.get_Some_0()@.pcell == self.cell_id + &&& self.local_updates matches Some(local_updates) + &&& local_updates.instance_id() == inst.id() + &&& local_updates.value().is_Init() + &&& local_updates.value().get_Init_op() == op + &&& self.batch_perms matches Some(batch_perms) + &&& batch_perms@.pcell == self.cell_id &&& self.cell_id == batch_cell - &&& self.batch_perms.get_Some_0().mem_contents().is_uninit() + &&& batch_perms.mem_contents().is_uninit() &&& self.fc_clients.instance_id() == fc_inst.id() &&& self.fc_clients.key() == tid &&& self.fc_clients.value().is_Idle() @@ -514,15 +514,15 @@ impl FCClientRequestResponseGhost
{ pub open spec fn enqueue_op_post(&self, pre: FCClientRequestResponseGhost
) -> bool recommends - pre.local_updates.is_Some(), + pre.local_updates.is_some(), { &&& self.fc_clients.value().is_Waiting() - &&& self.fc_clients.value().get_Waiting_0() == pre.local_updates.get_Some_0().key() + &&& self.fc_clients.value().get_Waiting_0() == pre.local_updates.unwrap().key() &&& self.fc_clients.instance_id() == pre.fc_clients.instance_id() &&& self.fc_clients.key() == pre.fc_clients.key() &&& self.cell_id == pre.cell_id - &&& self.batch_perms.is_None() - &&& self.local_updates.is_None() + &&& self.batch_perms.is_none() + &&& self.local_updates.is_none() } pub open spec fn dequeue_resp_pre( @@ -534,8 +534,8 @@ impl FCClientRequestResponseGhost
{ &&& self.fc_clients.key() == tid &&& self.fc_clients.instance_id() == fc_inst.id() &&& self.fc_clients.value().is_Waiting() - &&& self.batch_perms.is_None() - &&& self.local_updates.is_None() + &&& self.batch_perms.is_none() + &&& self.local_updates.is_none() &&& self.cell_id == batch_cell } @@ -545,21 +545,21 @@ impl FCClientRequestResponseGhost
{ ret: Option, inst: UnboundedLog::Instance
, ) -> bool { - &&& ret.is_Some() ==> { + &&& ret matches Some(ret) ==> { &&& self.cell_id == pre.cell_id - &&& self.batch_perms.is_Some() - &&& self.batch_perms.get_Some_0().mem_contents().is_uninit() - &&& self.batch_perms.get_Some_0()@.pcell == self.cell_id - &&& self.local_updates.is_Some() - &&& self.local_updates.get_Some_0().instance_id() == inst.id() - &&& self.local_updates.get_Some_0().value().is_Done() - &&& self.local_updates.get_Some_0().key() == pre.fc_clients.value().get_Waiting_0() - &&& self.local_updates.get_Some_0().value().get_Done_ret() == ret.get_Some_0() + &&& self.batch_perms matches Some(batch_perms) + &&& batch_perms.mem_contents().is_uninit() + &&& batch_perms@.pcell == self.cell_id + &&& self.local_updates matches Some(local_updates) + &&& local_updates.instance_id() == inst.id() + &&& local_updates.value().is_Done() + &&& local_updates.key() == pre.fc_clients.value().get_Waiting_0() + &&& local_updates.value().get_Done_ret() == ret &&& self.fc_clients.instance_id() == pre.fc_clients.instance_id() &&& self.fc_clients.key() == pre.fc_clients.key() &&& self.fc_clients.value().is_Idle() } - &&& ret.is_None() ==> { + &&& ret.is_none() ==> { &&& self == pre } } diff --git a/verified-node-replication/src/exec/log.rs b/verified-node-replication/src/exec/log.rs index 939e825..c2bfd2a 100644 --- a/verified-node-replication/src/exec/log.rs +++ b/verified-node-replication/src/exec/log.rs @@ -273,10 +273,10 @@ impl NrLog
{ -log_size <= logical_log_idx <= 0, slog_entries.len() == log_idx, cell_ids.len() == log_idx, - forall|i| 0 <= i < log_idx ==> (#[trigger] slog_entries[i]).is_Some(), + forall|i| 0 <= i < log_idx ==> (#[trigger] slog_entries[i]).is_some(), forall|i| 0 <= i < log_idx ==> #[trigger] cell_ids[i] == ( - #[trigger] slog_entries[i]).get_Some_0().id(), + #[trigger] slog_entries[i]).unwrap().id(), forall|i| -log_size <= i < logical_log_idx <==> #[trigger] contents.contains_key(i), forall|i| #[trigger] contents.contains_key(i) ==> stored_type_inv( @@ -367,12 +367,12 @@ impl NrLog
{ &&& cb_alive_bits[i].value() == false &&& cb_alive_bits[i].instance_id() == cyclic_buffer_instance.id() }, - forall|i| 0 <= i < log_idx ==> slog_entries.spec_index(i).is_None(), + forall|i| 0 <= i < log_idx ==> slog_entries.spec_index(i).is_none(), forall|i| #![trigger slog_entries[i]] log_idx <= i < log_size ==> { - &&& slog_entries[i].is_Some() - &&& slog_entries[i].get_Some_0().id() == cell_ids[i] + &&& slog_entries[i] matches Some(entry) + &&& entry.id() == cell_ids[i] }, decreases log_size - log_idx { @@ -382,7 +382,7 @@ impl NrLog
{ } let mut log_entry = Option::None; slog_entries.set_and_swap(log_idx, &mut log_entry); - assert(log_entry.is_Some()); + assert(log_entry.is_some()); let log_entry = log_entry.unwrap(); let cb_inst = Tracked(cyclic_buffer_instance.clone()); let entry = BufferEntry { @@ -1527,7 +1527,7 @@ impl NrLog
{ } else { // case: remote dispatch proof { - assert(stored_entry.log_entry.get_Some_0().value().node_id != nid); + assert(stored_entry.log_entry.unwrap().value().node_id != nid); if let Option::Some(e) = &stored_entry.log_entry { assert(e.value().node_id != nid); // assert(ghost_replica@.key == nid as nat); diff --git a/verified-node-replication/src/exec/replica.rs b/verified-node-replication/src/exec/replica.rs index 473b5de..4158e67 100644 --- a/verified-node-replication/src/exec/replica.rs +++ b/verified-node-replication/src/exec/replica.rs @@ -237,7 +237,7 @@ pub open spec fn wf(&self) -> bool { // v != 0 means lock is not taken, if it's not taken, the ghost state is Some &&& (v == 0) <==> g.is_some() // - &&& (g.is_some() ==> g.get_Some_0().inv(flat_combiner_instance@, responses.id(), collected_operations.id(), collected_operations_per_thread.id())) + &&& (g matches Some(g) ==> g.inv(flat_combiner_instance@, responses.id(), collected_operations.id(), collected_operations_per_thread.id())) } // invariant on num_threads with (flat_combiner_instance) specifically (self.num_threads.0) is (v: u64, g: Tracked) { @@ -462,7 +462,7 @@ impl Replica
{ self.wf(), ensures result.0 ==> result.1@.is_some(), - result.0 ==> result.1@.get_Some_0().inv( + result.0 ==> result.1@.unwrap().inv( self.flat_combiner_instance@, self.responses.id(), self.collected_operations.id(), @@ -783,7 +783,7 @@ impl Replica
{ self.flat_combiner_instance.borrow().pre_combiner_collect_request(&g.slots, flat_combiner.borrow()); rids_match_add_rid(flat_combiner.view().value().get_Collecting_0(), request_ids, - 0, flat_combiner.view().value().get_Collecting_0().len(), 0, request_ids.len(),g.update.get_Some_0().key()); + 0, flat_combiner.view().value().get_Collecting_0().len(), 0, request_ids.len(),g.update.unwrap().key()); update_req = g.update; batch_perms = g.batch_perms; @@ -998,7 +998,7 @@ impl Replica
{ old(self).replica_token@ == self.replica_token@, old(self).unbounded_log_instance@ == self.unbounded_log_instance@, old(self).cyclic_buffer_instance@ == self.cyclic_buffer_instance@, - res.is_Some() ==> res.get_Some_0().wf(self), + res matches Some(res) ==> res.wf(self), { self.thread_tokens.pop() } @@ -1234,7 +1234,7 @@ impl Replica
{ context.flat_combiner_instance@ == self.flat_combiner_instance@, context.unbounded_log_instance@ == self.unbounded_log_instance@, 0 <= iter <= RESPONSE_CHECK_INTERVAL, - r.is_None() ==> context_ghost_new@.dequeue_resp_pre( + r.is_none() ==> context_ghost_new@.dequeue_resp_pre( context.batch.0.id(), tid as nat, self.flat_combiner_instance@, diff --git a/verified-node-replication/src/exec/rwlock.rs b/verified-node-replication/src/exec/rwlock.rs index b58b623..a2b52a8 100644 --- a/verified-node-replication/src/exec/rwlock.rs +++ b/verified-node-replication/src/exec/rwlock.rs @@ -288,8 +288,8 @@ impl RwLock { while !acquired invariant self.wf(), - acquired ==> token.is_Some() && token.get_Some_0().instance_id() == self.inst@.id() - && token.get_Some_0().value() == 0, + acquired ==> (token matches Some(token) && token.instance_id() == self.inst@.id() + && token.value() == 0), { let result = atomic_with_ghost!( @@ -297,7 +297,7 @@ impl RwLock { returning res; ghost g => { - if res.is_Ok() { + if res.is_ok() { token = Option::Some(self.inst.borrow().exc_start(&mut g)); } }); diff --git a/verified-node-replication/src/exec/utils.rs b/verified-node-replication/src/exec/utils.rs index 5137c24..3306556 100644 --- a/verified-node-replication/src/exec/utils.rs +++ b/verified-node-replication/src/exec/utils.rs @@ -25,9 +25,9 @@ pub open spec fn rids_match( if bools_end == bools_start { rids_end == rids_start } else { - if bools[bools_end - 1].is_Some() { + if let Some(end) = bools[bools_end - 1] { &&& rids_end > rids_start - &&& rids[rids_end - 1] == bools[bools_end - 1].get_Some_0() + &&& rids[rids_end - 1] == end &&& rids_match( bools, rids, @@ -62,7 +62,7 @@ pub proof fn rids_match_add_none( if bools_end == bools_start { assert(rids_match(bools_new, rids, bools_start, bools_end, rids_start, rids_end)); } else { - if bools[bools_end - 1].is_Some() { + if bools[bools_end - 1].is_some() { rids_match_add_none( bools, rids, @@ -113,7 +113,7 @@ pub proof fn rids_match_add_rid( if bools_end == bools_start { assert(rids_match(bools_new, rids_new, bools_start, bools_end, rids_start, rids_end)); } else { - if bools[bools_end - 1].is_Some() { + if bools[bools_end - 1].is_some() { rids_match_add_rid( bools, rids, @@ -154,9 +154,9 @@ pub proof fn rids_match_pop( rids_match(bools, rids, bools_start, bools_end, rids_start, rids_end) }, bools_end > bools_start ==> { - &&& bools[bools_start as int].is_Some() ==> { + &&& bools[bools_start as int] matches Some(start) ==> { &&& rids_start < rids_end - &&& rids[rids_start as int] == bools[bools_start as int].get_Some_0() + &&& rids[rids_start as int] == start &&& rids_match( bools, rids, @@ -166,7 +166,7 @@ pub proof fn rids_match_pop( rids_end, ) } - &&& bools[bools_start as int].is_None() ==> { + &&& bools[bools_start as int].is_none() ==> { &&& rids_match( bools, rids, @@ -181,7 +181,7 @@ pub proof fn rids_match_pop( { if bools_end == bools_start { } else { - if bools[bools_end - 1].is_Some() { + if bools[bools_end - 1].is_some() { rids_match_pop( bools, rids, diff --git a/verified-node-replication/src/lib.rs b/verified-node-replication/src/lib.rs index 4b6419a..eb33405 100644 --- a/verified-node-replication/src/lib.rs +++ b/verified-node-replication/src/lib.rs @@ -263,7 +263,7 @@ pub trait NodeReplicatedT: Sized { old(self).wf(), ensures self.wf(), - result.is_Some() ==> result.get_Some_0().wf(&self.replicas()[replica_id as int]), + result matches Some(r) ==> r.wf(&self.replicas()[replica_id as int]), ; /// executes an update operation against the data structure. @@ -281,13 +281,13 @@ pub trait NodeReplicatedT: Sized { tkn.wf(&self.replicas().spec_index(tkn.replica_id_spec() as int)), is_update_ticket(ticket@, op, self.unbounded_log_instance()), ensures - result.is_Ok() ==> is_update_stub( - result.get_Ok_0().2@, + result matches Ok(ok) ==> is_update_stub( + ok.2@, ticket@.key(), - result.get_Ok_0().0, + ok.0, self.unbounded_log_instance(), - ) && result.get_Ok_0().1.wf(&self.replicas().spec_index(tkn.replica_id_spec() as int)), - result.is_Err() ==> result.get_Err_0().1 == ticket && result.get_Err_0().0 == tkn, + ) && ok.1.wf(&self.replicas().spec_index(tkn.replica_id_spec() as int)), + result matches Err(err) ==> err == (tkn, ticket), ; /// executes a read-only operation against the data structure. @@ -305,13 +305,13 @@ pub trait NodeReplicatedT: Sized { tkn.wf(&self.replicas()[tkn.replica_id_spec() as int]), is_readonly_ticket(ticket@, op, self.unbounded_log_instance()), ensures - result.is_Ok() ==> is_readonly_stub( - result.get_Ok_0().2@, + result matches Ok(ok) ==> is_readonly_stub( + ok.2@, ticket@.key(), - result.get_Ok_0().0, + ok.0, self.unbounded_log_instance(), - ) && result.get_Ok_0().1.wf(&self.replicas()[tkn.replica_id_spec() as int]), - result.is_Err() ==> result.get_Err_0().1 == ticket && result.get_Err_0().0 == tkn, + ) && ok.1.wf(&self.replicas()[tkn.replica_id_spec() as int]), + result matches Err(err) ==> err == (tkn, ticket), ; } diff --git a/verified-node-replication/src/spec/cyclicbuffer.rs b/verified-node-replication/src/spec/cyclicbuffer.rs index 5236622..d44b692 100644 --- a/verified-node-replication/src/spec/cyclicbuffer.rs +++ b/verified-node-replication/src/spec/cyclicbuffer.rs @@ -60,13 +60,13 @@ pub open spec fn stored_type_inv( &&& st.cell_perms.mem_contents().is_init() &&& st.cell_perms@.pcell == cell_id &&& idx >= 0 ==> { - &&& st.log_entry.is_Some() - &&& st.log_entry.get_Some_0().key() == idx - &&& st.log_entry.get_Some_0().instance_id() == unbounded_log_instance.id() - &&& st.cell_perms.mem_contents().value().is_Some() - &&& st.cell_perms.mem_contents().value().get_Some_0().node_id as NodeId - == st.log_entry.get_Some_0().value().node_id - &&& st.cell_perms.mem_contents().value().get_Some_0().op == st.log_entry.get_Some_0().value().op + &&& st.log_entry matches Some(log_entry) + &&& log_entry.key() == idx + &&& log_entry.instance_id() == unbounded_log_instance.id() + &&& st.cell_perms.mem_contents().value() matches Some(cell_perms_value) + &&& cell_perms_value.node_id as NodeId + == log_entry.value().node_id + &&& cell_perms_value.op == log_entry.value().op } &&& idx < 0 ==> { &&& true diff --git a/verified-node-replication/src/spec/flat_combiner.rs b/verified-node-replication/src/spec/flat_combiner.rs index 9a9ea16..6938aec 100644 --- a/verified-node-replication/src/spec/flat_combiner.rs +++ b/verified-node-replication/src/spec/flat_combiner.rs @@ -61,8 +61,8 @@ impl CombinerState { 0 <= tid < self.req_len(), { match self { - CombinerState::Collecting(reqs) => reqs[tid as int].is_None(), - CombinerState::Responding(reqs, _) => reqs[tid as int].is_None(), + CombinerState::Collecting(reqs) => reqs[tid as int].is_none(), + CombinerState::Responding(reqs, _) => reqs[tid as int].is_none(), } } @@ -71,8 +71,8 @@ impl CombinerState { 0 <= tid < self.req_len(), { match self { - CombinerState::Collecting(reqs) => reqs[tid as int].is_Some(), - CombinerState::Responding(reqs, _) => reqs[tid as int].is_Some(), + CombinerState::Collecting(reqs) => reqs[tid as int].is_some(), + CombinerState::Responding(reqs, _) => reqs[tid as int].is_some(), } } } @@ -146,13 +146,13 @@ FlatCombiner { match self.combiner { CombinerState::Collecting(elems) => { // fff - &&& (forall |i: nat| 0 <= i < elems.len() && elems[i as int].is_None() + &&& (forall |i: nat| 0 <= i < elems.len() && elems[i as int].is_none() ==> !(#[trigger] self.slots[i]).is_InProgress()) //Self::slot_in_progress(self.slots, i))) // everything above is not in progress &&& (forall |i: nat| elems.len() <= i < self.num_threads ==> !self.slots[i].is_InProgress()) }, CombinerState::Responding(elems, idx) => { - &&& (forall |i: nat| 0 <= i < elems.len() && elems[i as int].is_None() + &&& (forall |i: nat| 0 <= i < elems.len() && elems[i as int].is_none() ==> !(#[trigger] self.slots[i]).is_InProgress()) //Self::slot_in_progress(self.slots, i))) &&& (forall |i: nat| 0 <= i < idx ==> !self.slots[i].is_InProgress()) }, @@ -163,12 +163,12 @@ FlatCombiner { pub fn inv_combiner_request_ids(&self) -> bool { match self.combiner { CombinerState::Collecting(elems) => { - forall |i:nat| (0 <= i < elems.len() && elems[i as int].is_Some()) - ==> (#[trigger] self.slots[i]).is_InProgress() && (#[trigger] self.slots[i]).get_InProgress_0() == elems[i as int ].get_Some_0() + forall |i:nat| (0 <= i < elems.len() && elems[i as int].is_some()) + ==> (#[trigger] self.slots[i]).is_InProgress() && (#[trigger] self.slots[i]).get_InProgress_0() == elems[i as int].unwrap() }, CombinerState::Responding(elems, idx) => { - forall |i:nat| idx <= i < elems.len() && elems[i as int].is_Some() - ==> (#[trigger] self.slots[i]).is_InProgress() && (#[trigger] self.slots[i]).get_InProgress_0() == elems[i as int].get_Some_0() + forall |i:nat| idx <= i < elems.len() && elems[i as int].is_some() + ==> (#[trigger] self.slots[i]).is_InProgress() && (#[trigger] self.slots[i]).get_InProgress_0() == elems[i as int].unwrap() }, } } @@ -280,7 +280,7 @@ FlatCombiner { update combiner = CombinerState::Responding(pre.combiner.get_Responding_0(), tid + 1); remove slots -= [ tid => let r ]; assert let SlotState::InProgress(rid) = r; - assert pre.combiner.get_Responding_0()[tid as int].get_Some_0() == rid; + assert pre.combiner.get_Responding_0()[tid as int].unwrap() == rid; add slots += [ tid => SlotState::Response(rid) ]; } } diff --git a/verified-node-replication/src/spec/rwlock.rs b/verified-node-replication/src/spec/rwlock.rs index cb8de79..22ba2c6 100644 --- a/verified-node-replication/src/spec/rwlock.rs +++ b/verified-node-replication/src/spec/rwlock.rs @@ -82,7 +82,7 @@ tokenized_state_machine!{ remove exc_pending -= Some(pre.rc_width); add exc_guard += Some(()); - birds_eye let x = pre.storage.get_Some_0(); + birds_eye let x = pre.storage.unwrap(); withdraw storage -= Some(x); assert(pre.user_inv.contains(x)); @@ -120,7 +120,7 @@ tokenized_state_machine!{ require(!pre.exc_locked); remove shared_pending -= {r}; - birds_eye let t = pre.storage.get_Some_0(); + birds_eye let t = pre.storage.unwrap(); add shared_guard += {(r, t)}; assert(pre.user_inv.contains(t)); @@ -166,8 +166,8 @@ tokenized_state_machine!{ #[invariant] pub fn sto_user_inv(&self) -> bool { - self.storage.is_Some() ==> - self.user_inv.contains(self.storage.get_Some_0()) + self.storage matches Some(storage) ==> + self.user_inv.contains(storage) } #[invariant] @@ -178,11 +178,11 @@ tokenized_state_machine!{ #[invariant] pub fn exc_inv(&self) -> bool { - &&& self.exc_locked <==> (self.exc_pending.is_Some() || self.exc_guard.is_Some()) - &&& self.storage.is_Some() <==> self.exc_guard.is_None() + &&& self.exc_locked <==> (self.exc_pending.is_some() || self.exc_guard.is_some()) + &&& self.storage.is_some() <==> self.exc_guard.is_none() &&& if let Option::Some(cur_r) = self.exc_pending { &&& 0 <= cur_r <= self.rc_width - &&& self.exc_guard.is_None() + &&& self.exc_guard.is_none() &&& forall |x| self.shared_guard.count(x) > 0 ==> !(0 <= x.0 < cur_r) } else { true @@ -239,7 +239,7 @@ tokenized_state_machine!{ #[inductive(exc_check_count)] fn exc_check_count_inductive(pre: Self, post: Self) { - let prev_r = pre.exc_pending.get_Some_0(); + let prev_r = pre.exc_pending.unwrap(); assert forall |x| #[trigger] post.shared_guard.count(x) > 0 && x.0 == prev_r implies false by { @@ -264,7 +264,7 @@ tokenized_state_machine!{ #[inductive(shared_finish)] fn shared_finish_inductive(pre: Self, post: Self, r: int) { - let t = pre.storage.get_Some_0(); + let t = pre.storage.unwrap(); assert forall |r0| 0 <= r0 < post.rc_width implies #[trigger] post.ref_counts.index(r0) ==