Agree with your overall point. I made some changes to extend the current paradigm a bit: https://github.com/bneb/lattice/blob/main/docs/tutorial/09-c...

---

Invariants aren't always inferred automatically. When they aren't, they can be made explicit for Z3 to check.

At the moment, bubble sort with array-content invariants is fully provable:

  fn bubble_sort(arr: Ptr<i32>, n: i64)
      requires n > 0
      ensures forall i in 0..(n-1) => arr[i] <= arr[i+1]
  {
      for i in 0..n {
          invariant forall k in 0..(i-1) => arr[k] <= arr[k+1];
          // bubble pass
      }
  }

Z3 proves the base case (vacuously true at i=0) and the inductive step for each iteration. Both loops have fixed trip counts regardless of data, so the frame axioms are concrete. At concrete sizes the compiler unrolls the loop: for i in 0..4 produces 8 Z3 checks (4 iterations × 2), all proven at compile time, outputting Z3: 8/8 checks proven (100%), 0 deferred to runtime.

And insertion sort is partially provable:

This starts with the same `forall` invariant structure. After the base case, the outer for-loop inductive step is wired but the inner while-loop's trip count depends on the data which can't be determined statically for which indices were modified, so the frame axioms can't fully constrain the array state. This would require splitting on the case for the while condition, which is future work, and wasn't part of my v1.0.0 plans.