From df8d5ca6bb34fd45b3f6238c2b2b74915054be58 Mon Sep 17 00:00:00 2001 From: Matthias Date: Tue, 25 Jun 2024 21:01:43 +0000 Subject: [PATCH] Add an invariant preserved by dispatch_mut to the Dispatch trait --- verified-node-replication/src/exec/log.rs | 10 ++++++++++ verified-node-replication/src/exec/replica.rs | 7 +++++-- verified-node-replication/src/lib.rs | 9 +++++++++ 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/verified-node-replication/src/exec/log.rs b/verified-node-replication/src/exec/log.rs index e361d8e..b459b05 100644 --- a/verified-node-replication/src/exec/log.rs +++ b/verified-node-replication/src/exec/log.rs @@ -706,6 +706,7 @@ impl NrLog
{ ) -> (result: Tracked>) requires self.wf(), + old(actual_replica).inv(), replica_token@ < self.local_versions.len(), old(responses).len() == 0, ghost_data@.append_pre( @@ -717,6 +718,7 @@ impl NrLog
{ ), operations.len() <= MAX_REQUESTS, ensures + actual_replica.inv(), result@.append_post( ghost_data@, replica_token@, @@ -735,6 +737,7 @@ impl NrLog
{ loop invariant self.wf(), + actual_replica.inv(), 0 <= waitgc <= WARN_THRESHOLD, 0 <= iteration <= WARN_THRESHOLD, responses.len() == 0, @@ -1072,6 +1075,7 @@ impl NrLog
{ ) -> (res: Tracked>) requires self.wf(), + old(actual_replica).inv(), replica_token.wf(self.num_replicas@), ghost_data@.advance_head_pre( replica_token.id_spec(), @@ -1081,6 +1085,7 @@ impl NrLog
{ self.cyclic_buffer_instance@, ), ensures + actual_replica.inv(), res@.advance_head_post( ghost_data@, replica_token.id_spec(), @@ -1095,6 +1100,7 @@ impl NrLog
{ loop invariant self.wf(), + actual_replica.inv(), replica_token.wf(self.num_replicas@), ghost_data_new@.cb_combiner@@.value.is_Idle(), ghost_data_new@.combiner@@.value.is_Placed() ==> ghost_data_new@.pre_exec( @@ -1264,6 +1270,7 @@ impl NrLog
{ ghost_data: Tracked>, ) -> (result: Tracked>) requires + old(actual_replica).inv(), self.wf(), replica_token@ < self.local_versions.len(), ghost_data@.execute_pre( @@ -1274,6 +1281,7 @@ impl NrLog
{ self.cyclic_buffer_instance@, ), ensures + actual_replica.inv(), result@.execute_post( ghost_data@, replica_token@, @@ -1370,6 +1378,7 @@ impl NrLog
{ while local_version < global_tail invariant self.wf(), + actual_replica.inv(), ghost_data.combiner@@.value.is_Placed() ==> { &&& ghost_data.combiner@@.value.get_Placed_queued_ops() == request_ids &&& combiner@.value.get_Loop_queued_ops() == request_ids @@ -1428,6 +1437,7 @@ impl NrLog
{ while !is_alive invariant self.wf(), + actual_replica.inv(), local_version < global_tail, phys_log_idx < self.slog.len(), phys_log_idx as nat == self.index_spec(local_version as nat), diff --git a/verified-node-replication/src/exec/replica.rs b/verified-node-replication/src/exec/replica.rs index 0791671..5a387cd 100644 --- a/verified-node-replication/src/exec/replica.rs +++ b/verified-node-replication/src/exec/replica.rs @@ -225,7 +225,7 @@ pub open spec fn wf(&self) -> bool { &&& self.data.0.max_threads() == self.contexts.len() &&& 0 <= self.spec_id() < MAX_REPLICAS &&& self.data.0.wf() - &&& (forall |v: ReplicatedDataStructure
| (#[trigger] self.data.0.inv(v)) == v.wf(self.spec_id(), self.unbounded_log_instance@, self.cyclic_buffer_instance@)) + &&& (forall |v: ReplicatedDataStructure
| (#[trigger] self.data.0.inv(v)) == (v.wf(self.spec_id(), self.unbounded_log_instance@, self.cyclic_buffer_instance@) && v.data.inv())) &&& self.flat_combiner_instance@.num_threads() == MAX_THREADS_PER_REPLICA &&& (forall |i| #![trigger self.thread_tokens[i]] 0 <= i < self.thread_tokens.len() ==> { @@ -316,7 +316,10 @@ impl Replica
{ )); // TODO: get the right spec function in there! let ghost data_structure_inv = |s: ReplicatedDataStructure
| - { s.wf(replica_token.id_spec(), unbounded_log_instance, cyclic_buffer_instance) }; + { + s.wf(replica_token.id_spec(), unbounded_log_instance, cyclic_buffer_instance) + && s.data.inv() + }; let data = CachePadded( RwLock::new( MAX_THREADS_PER_REPLICA, diff --git a/verified-node-replication/src/lib.rs b/verified-node-replication/src/lib.rs index bb56d55..e335b9c 100644 --- a/verified-node-replication/src/lib.rs +++ b/verified-node-replication/src/lib.rs @@ -154,6 +154,7 @@ pub trait Dispatch: Sized { fn init() -> (res: Self) ensures res@ == Self::init_spec(), + res.inv(), ; /// Clones a write operation to be copied to and read from the shared log. @@ -170,13 +171,18 @@ pub trait Dispatch: Sized { /// Executes a read-only operation against the data structure and returns the result. fn dispatch(&self, op: Self::ReadOperation) -> (result: Self::Response) + requires + self.inv(), ensures Self::dispatch_spec(self@, op) == result, ; /// Executes a write operation against the data structure and returns the result. fn dispatch_mut(&mut self, op: Self::WriteOperation) -> (result: Self::Response) + requires + old(self).inv(), ensures + self.inv(), Self::dispatch_mut_spec(old(self)@, op) == (self@, result), ; @@ -191,6 +197,9 @@ pub trait Dispatch: Sized { Self::View, Self::Response, ); + + /// An invariant that is preserved by [`Dispatch::dispatch_mut`] + spec fn inv(&self) -> bool; } ////////////////////////////////////////////////////////////////////////////////////////////////////