Add an invariant preserved by dispatch_mut to the Dispatch trait

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

@@ -706,6 +706,7 @@ impl<DT: Dispatch> NrLog<DT> {
     ) -> (result: Tracked<NrLogAppendExecDataGhost<DT>>)
         requires
             self.wf(),
+            old(actual_replica).inv(),
             replica_token@ < self.local_versions.len(),
             old(responses).len() == 0,
             [email protected]_pre(
@@ -717,6 +718,7 @@ impl<DT: Dispatch> NrLog<DT> {
             ),
             operations.len() <= MAX_REQUESTS,
         ensures
+            actual_replica.inv(),
             [email protected]_post(
                 ghost_data@,
                 replica_token@,
@@ -735,6 +737,7 @@ impl<DT: Dispatch> NrLog<DT> {
         loop
             invariant
                 self.wf(),
+                actual_replica.inv(),
                 0 <= waitgc <= WARN_THRESHOLD,
                 0 <= iteration <= WARN_THRESHOLD,
                 responses.len() == 0,
@@ -1072,6 +1075,7 @@ impl<DT: Dispatch> NrLog<DT> {
     ) -> (res: Tracked<NrLogAppendExecDataGhost<DT>>)
         requires
             self.wf(),
+            old(actual_replica).inv(),
             replica_token.wf(self.num_replicas@),
             [email protected]_head_pre(
                 replica_token.id_spec(),
@@ -1081,6 +1085,7 @@ impl<DT: Dispatch> NrLog<DT> {
                 self.cyclic_buffer_instance@,
             ),
         ensures
+            actual_replica.inv(),
             [email protected]_head_post(
                 ghost_data@,
                 replica_token.id_spec(),
@@ -1095,6 +1100,7 @@ impl<DT: Dispatch> NrLog<DT> {
         loop
             invariant
                 self.wf(),
+                actual_replica.inv(),
                 replica_token.wf(self.num_replicas@),
                 [email protected]_combiner@@.value.is_Idle(),
                 [email protected]@@.value.is_Placed() ==> [email protected]_exec(
@@ -1264,6 +1270,7 @@ impl<DT: Dispatch> NrLog<DT> {
         ghost_data: Tracked<NrLogAppendExecDataGhost<DT>>,
     ) -> (result: Tracked<NrLogAppendExecDataGhost<DT>>)
         requires
+            old(actual_replica).inv(),
             self.wf(),
             replica_token@ < self.local_versions.len(),
             [email protected]_pre(
@@ -1274,6 +1281,7 @@ impl<DT: Dispatch> NrLog<DT> {
                 self.cyclic_buffer_instance@,
             ),
         ensures
+            actual_replica.inv(),
             [email protected]_post(
                 ghost_data@,
                 replica_token@,
@@ -1370,6 +1378,7 @@ impl<DT: Dispatch> NrLog<DT> {
         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
                     &&& [email protected]_Loop_queued_ops() == request_ids
@@ -1428,6 +1437,7 @@ impl<DT: Dispatch> NrLog<DT> {
             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),

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<DT>| (#[trigger] self.data.0.inv(v)) == v.wf(self.spec_id(), self.unbounded_log_instance@, self.cyclic_buffer_instance@))
+        &&& (forall |v: ReplicatedDataStructure<DT>| (#[trigger] self.data.0.inv(v)) == (v.wf(self.spec_id(), self.unbounded_log_instance@, self.cyclic_buffer_instance@) && v.data.inv()))
 
         &&& self[email protected]_threads() == MAX_THREADS_PER_REPLICA
         &&& (forall |i| #![trigger self.thread_tokens[i]] 0 <= i < self.thread_tokens.len() ==> {
@@ -316,7 +316,10 @@ impl<DT: Dispatch> Replica<DT> {
         ));
         // TODO: get the right spec function in there!
         let ghost data_structure_inv = |s: ReplicatedDataStructure<DT>|
-            { 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,

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;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////