[valentynkit]

Bounds and div-by-zero are the easy wins; the real tax with contract systems is the loop invariant Z3 can't infer on its own, where you end up hand-writing an `ensures` longer than the function body. What's the gnarliest invariant you had to spell out by hand to get one of those kernels to verify?

[bneb-dev]

For loops already worked but might not have been documented correctly. I just shipped the functionality for `while` loops now, auto-infer works for common cases of invariants:

  let mut i = 0;
  while i < 5 {
    arr[i] = val;
    i += 1;
  }

So in that case, the compiler detects `i < N` with monotonic increment and synthesizes `i >= 0 && i < N` automatically.

(Works with `<`, `<=`, `i += 1`, and `i = i + 1` via the same mechanism as for-loop induction variables.)

Complex loops (`while i + j < n`, `while p.addr() != 0`) require syntax that I have slopped together an explicit `invariant` keyword that I am not 100% happy with, but will refine later. Z3 checks base case + inductive step via Hoare logic and reports counterexamples on failure.

---

RE: "gnarliest invariant"

`ensures(result != 0)` on the SYN cookie in the kernel contract for the OS project in the monorepo.

[derdi]

The more interesting loop invariants aren't the ones about the loop counter but about the contents of the array. If you require `forall i, array[i] == value` after that loop, will the system come up with the loop invariant about the prefix of the array for any given `i`? What about something like bubblesort or insertion sort?

[bneb-dev]

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.

[bneb-dev]

Made updates directly influenced by your input. Please feel free to follow up in Github!

See https://github.com/bneb/lattice/blob/main/docs/deep-dives/z3...