len() implementation without overflow errors

[fpoli]

Viktor Kuncak (@vkuncak) suggested the following trick to implement a len() method that verifies with overflow checks enabled. They used it in Stainless:

impl Link {
    #[pure]
    #[ensures(result <= usize::MAX - 1)]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => {
              let len1 = node.next.len();
              if len1 == usize::MAX - 1 {
                len1
              } else {
                len1 + 1
              }
            }
        }
    }
}

[CleveGreen]

Using saturating arithmetic works for implementing len with overflow checks, but it complicates other specifications that depend on it.

One way to avoid enabling overflow checks for the entire project is to write an increment function and mark it as trusted, even though it might feel a bit unsatisfactory.

Perhaps dynamically sized number types would help with this? I was planning on taking a swing on implementing and verifying these tomorrow.