Make compatible with new Verus that enforces termination checking

Author: jaylorch

ironsht/src/args_t.rs

@@ -31,6 +31,8 @@ ensures
             i <= v.len(),
             i == out.len(),
             forall |j| #![auto] 0 <= j < i  ==> out@[j] == v@[j],
+        decreases
+            v.len() - i,
     {
         out.push(v[i]);
         i = i + 1;

ironsht/src/delegation_map_v.rs

@@ -233,6 +233,8 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedVec<K> {
                 deleted_set == old(self)@.subrange(start as int, start as int + deleted as int).to_set(),
                 deleted_set.len() == deleted,
                 old(self)@.to_set() == self@.to_set() + deleted_set,
+            decreases
+                end - start - deleted,
         {
             let ghost mut old_deleted_set;
             let ghost mut old_deleted_seq;
@@ -299,6 +301,8 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedVec<K> {
             invariant
                 0 <= index <= self@.len(),
                 forall |i| 0 <= i < index ==> (#[trigger] self@.index(i).cmp_spec(k)).lt()
+            decreases
+               self@.len() - index
         {
             index = index + 1;
         }
@@ -437,6 +441,8 @@ pub fn vec_erase<A>(v: &mut Vec<A>, start: usize, end: usize)
             v@.len() == old(v)@.len() - deleted,
             0 <= deleted <= end - start,
             v@ == old(v)@.subrange(0, start as int) + old(v)@.subrange(start as int + deleted as int, old(v)@.len() as int),
+        decreases
+            end - start - deleted
     {
         v.remove(start);
         deleted = deleted + 1;
@@ -539,6 +545,7 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedMap<K> {
         let mut i = 0;
         while i < self.keys.len()
             invariant forall |j| 0 <= j < i ==> self.keys@[j] != k,
+            decreases self.keys@.len() - i
         {
             //println!("Loop {} of find_key", i);
             if self.keys.index(i).cmp(&k).is_eq() {
@@ -571,8 +578,11 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedMap<K> {
         while i <= hi
             invariant 
                 lo <= i,
+                self.keys@.len() <= usize::MAX,
                 hi < self.keys@.len() as usize == self.vals@.len(),
                 forall |j| #![auto] lo <= j < i ==> self.vals@[j]@ == v@,
+            decreases
+                self.keys@.len() - i
         {
             let eq = do_end_points_match(&self.vals[i], v);
             if  !eq {
@@ -788,6 +798,8 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedMap<K> {
              || (i < self.keys@.len() &&
                  !iter.geq_K(self.keys@.index(i as int)) &&
                  forall |j:nat| j < i ==> iter.geq_K(#[trigger]self.keys@.index(j as int))),
+            decreases
+                self.keys@.len() - i
         {
             if iter.lt(&KeyIterator::new(self.keys.index(i))) {
                 // Reached a key that's too large
@@ -884,6 +896,8 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedMap<K> {
                 self.valid(),
                 0 <= start <= self.keys@.len(),
                 forall |j| #![auto] 0 <= j < start ==> lo.above(self.keys@.index(j))
+            decreases
+                self.keys@.len() - start
         {
             start = start + 1;
         }
@@ -895,6 +909,8 @@ impl<K: KeyTrait + VerusClone> StrictlyOrderedMap<K> {
                 self.valid(),
                 start <= end <= self.keys@.len(),
                 forall |j| #![auto] start <= j < end ==> hi.above(self.keys@[j])
+            decreases
+                self.keys@.len() - end
         {
             end = end + 1;
         }

ironsht/src/host_impl_v.rs

@@ -302,11 +302,13 @@ impl HostState {
         let mut i: usize = 0;
 
         while i<args.len()
-        invariant
+          invariant
             i <= args.len(),
             end_points.len() == i,
             forall |j| #![auto] 0 <= j < i ==> parse_arg_as_end_point(abstractify_args(*args)[j]) == end_points@[j]@,
             forall |j| #![auto] 0 <= j < i ==> end_points@[j]@.valid_physical_address(),
+          decreases
+            args.len() - i
         {
             let end_point = Self::parse_end_point(&(*args)[i]);
             if !end_point.valid_physical_address() {

ironsht/src/main_t.rs

@@ -26,6 +26,7 @@ verus! {
 pub struct IronError {
 }
 
+#[verifier::exec_allows_no_decreases_clause]
 // net_impl comes from outside so this function can be verified.
 pub fn sht_main(netc: NetClient, args: Args) -> Result<(), IronError>
     requires

ironsht/src/marshal_ironsht_specific_v.rs

@@ -109,6 +109,8 @@ verus! {
               invariant
                 (0 < idx <= v.len()),
                 (forall |i: int, j: int| 0 <= i && i + 1 < idx && j == i+1 ==> #[trigger] ckeykvlt(v@[i], v@[j])),
+              decreases
+                v.len() - idx
             {
                 if v[idx - 1].k.ukey >= v[idx].k.ukey {
                     assert(!ckeykvlt(v@[idx as int-1], v@[idx as int]));

ironsht/src/marshal_v.rs

@@ -156,6 +156,8 @@ impl Marshalable for u64 {
         data@.subrange(0, old(data)@.len() as int) == old(data)@,
         data@.subrange(old(data)@.len() as int, data@.len() as int) == self.ghost_serialize().subrange(0, i as int),
         data@.len() == old(data)@.len() + i as int,
+      decreases
+        8 - i
     {
       assert(data@.subrange(old(data)@.len() as int, data@.len() as int) == data@.subrange(old(data)@.len() as int, old(data)@.len() + i as int));
 
@@ -343,6 +345,8 @@ impl Marshalable for Vec<u8> {
         data@.subrange(0, old(data)@.len() as int) == old(data)@,
         data@.subrange(old(data)@.len() as int, data@.len() as int) == self.ghost_serialize().subrange(0, i + init@),
         data@.len() == old(data)@.len() + i + init@,
+      decreases
+        self.len() - i
     {
       assert(data@.subrange(old(data)@.len() as int, data@.len() as int) == data@.subrange(old(data)@.len() as int, old(data)@.len() + i + init@));
 
@@ -633,6 +637,8 @@ impl<T: Marshalable> Marshalable for Vec<T> {
         res ==> (forall |x: T| self@.subrange(0, i as int).contains(x) ==> #[trigger] x.is_marshalable()),
         res ==> total_len as int <= usize::MAX,
         !res ==> !self.is_marshalable(),
+      decreases
+        self.len() - i + if res { 1int } else { 0int }
     {
       assert(res);
       res = res && self[i]._is_marshalable() && (usize::MAX - total_len >= self[i].serialized_size());
@@ -704,6 +710,8 @@ impl<T: Marshalable> Marshalable for Vec<T> {
                self@.subrange(0 as int, self@.len() as int).fold_left(0, |acc: int, x: T| acc + x.ghost_serialize().len()) <= usize::MAX,
         res == (self@.len() as usize).ghost_serialize().len() +
                self@.subrange(0 as int, i as int).fold_left(0, |acc: int, x: T| acc + x.ghost_serialize().len()),
+      decreases
+        self.len() - i
     {
       proof {
         let f = |x: T| x.ghost_serialize();
@@ -765,6 +773,8 @@ impl<T: Marshalable> Marshalable for Vec<T> {
             self@.subrange(0, i as int).fold_left(Seq::<u8>::empty(), |acc: Seq<u8>, x: T| acc + x.ghost_serialize()),
         forall |x: T| self@.contains(x) ==> #[trigger] x.is_marshalable(),
         data@.len() >= old(data)@.len(),
+      decreases
+        self.len() - i
     {
       self[i].serialize(data);
       i = i + 1;
@@ -833,6 +843,8 @@ impl<T: Marshalable> Marshalable for Vec<T> {
         len.ghost_serialize().len() +
           res@.fold_left(0, |acc: int, x: T| acc + x.ghost_serialize().len()) == end - start,
         accf@ == |acc: Seq<u8>, x: T| acc + x.ghost_serialize(),
+      decreases
+        len - i
     {
       let (x, end1) = match T::deserialize(data, end) { None => {
         return None;

ironsht/src/net_sht_v.rs

@@ -386,6 +386,8 @@ ensures
             send_log_entries_reflect_packets(net_events, cpackets@.subrange(0, i as int)),
             only_sent_marshalable_data(net_events),
             forall |i| 0 <= i < net_events.len() ==> net_events[i] is Send,
+        decreases
+            cpackets.len() - i
     {
         let cpacket: &CPacket = &cpackets[i];
         let (ok, Ghost(net_event)) = send_packet(cpacket, netc);

ironsht/src/seq_is_unique_v.rs

@@ -36,6 +36,8 @@ verus! {
                 i <= e1.len(),
                 e1.len() == e2.len(),
                 forall |j: int| 0 <= j && j < i ==> e1@[j] == e2@[j]
+            decreases
+                e1.len() - i
         {
             if e1[i] != e2[i] {
                 return false;
@@ -67,6 +69,8 @@ verus! {
                 i <= endpoints.len(),
                 forall |j: int, k: int| #![trigger endpoints@[j]@, endpoints@[k]@]
                     0 <= j && j < endpoints.len() && 0 <= k && k < i && j != k ==> endpoints@[j]@ != endpoints@[k]@,
+            decreases
+                endpoints.len() - i
         {
             let mut j: usize = 0;
             while j < endpoints.len()
@@ -78,6 +82,8 @@ verus! {
                     0 <= j,
                     j <= endpoints.len(),
                     forall |k: int| #![trigger endpoints@[k]@] 0 <= k && k < j && k != i ==> endpoints@[i as int]@ != endpoints@[k]@,
+                decreases
+                    endpoints.len() - j
             {
                 if i != j && do_end_points_match(&endpoints[i], &endpoints[j]) {
                     assert (!seq_is_unique(abstractify_end_points(*endpoints))) by {
@@ -107,6 +113,8 @@ verus! {
             invariant
                 0 <= j && j <= endpoints.len(),
                 forall |k: int| #![trigger endpoints@[k]@] 0 <= k && k < j ==> endpoint@ != endpoints@[k]@,
+            decreases
+                endpoints.len() - j
         {
             if do_end_points_match(endpoint, &endpoints[j]) {
                 assert (abstractify_end_points(*endpoints)[j as int] == endpoint@);

ironsht/src/single_delivery_model_v.rs

@@ -127,7 +127,7 @@ impl CSingleDelivery {
                 let mut i=0;
 
                 while i < ack_state.un_acked.len()
-                invariant
+                  invariant
                     0 <= i <= ack_state.un_acked.len(),
                     self.valid(),   // Everybody hates having to carry everything through here. :v(
                     src.abstractable(),
@@ -138,6 +138,8 @@ impl CSingleDelivery {
                     packets@.map_values(|p: CPacket| p@).to_set() ==
                         old(packets)@.map_values(|p: CPacket| p@).to_set() + self@.un_acked_messages_for_dest_up_to(src@, dst@, i as nat),
                     Self::packets_are_valid_messages(packets@),
+                  decreases
+                    ack_state.un_acked.len() - i
                 {
                     let ghost packets0_view = packets@;
 
@@ -552,7 +554,7 @@ impl CSingleDelivery {
         }
 
         while dst_i < dests.len()
-        invariant
+          invariant
             self.valid(),   // Everybody hates having to carry everything through here. :v(
             dests@.map_values(|ep: EndPoint| ep@).to_set() == self.send_state.epmap@.dom(), // NOTE: hard to figure this one out: this comes from postcondition of .keys(). Losing while context extra sad here because it was very painful to reconstruct.
             src.abstractable(),
@@ -562,6 +564,8 @@ impl CSingleDelivery {
             packets@.map_values(|p: CPacket| p@).to_set() ==
                 self@.un_acked_messages_for_dests(src@, dests@.subrange(0, dst_i as int).map_values(|ep: EndPoint| ep@).to_set()),
             Self::packets_are_valid_messages(packets@),
+          decreases
+            dests.len() - dst_i
         {
             let ghost packets0_view = packets@;
 

ironsht/src/single_delivery_state_v.rs

@@ -67,6 +67,8 @@ impl CAckState {
                 i <= self.un_acked.len(),
                 un_acked@.len() == i as nat,
                 forall |j: int| 0 <= j < i as nat ==> #[trigger] (un_acked@[j]@) == self.un_acked@[j]@
+            decreases
+                self.un_acked.len() - i
         {
             un_acked.push(self.un_acked[i].clone_up_to_view());
             i = i + 1;
@@ -171,7 +173,7 @@ impl CAckState {
                     true
                 },
             })
-        invariant
+          invariant
             self.valid(dst),
             self == old(self),
             i <= self.un_acked.len(),
@@ -181,6 +183,8 @@ impl CAckState {
             truncate_un_ack_list(abstractify_cmessage_seq(self.un_acked@.skip(i as int)), seqno_acked as nat)
                 == truncate_un_ack_list(abstractify_cmessage_seq(old(self).un_acked@), seqno_acked as nat),
             self.num_packets_acked + i <= seqno_acked,
+          decreases
+            self.un_acked.len() - i
         {
             assert( self.un_acked@.skip(i as int).skip(1) =~= self.un_acked@.skip((i + 1) as int) );
             i = i + 1;