`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
              }
            }
        }
    }
}