Refinements

A requires clause is a precondition; an ensures clause is a postcondition; a where clause refines a parameter or a field. Each compiles to an obligation the build has to discharge.

public function clamp(value: i32, lo: i32, hi: i32) -> i32
    requires hi >= lo
    ensures  result >= lo
    ensures  result <= hi
{
    if value < lo { return lo }
    else if value > hi { return hi }
    else { return value }
}

Some obligations are inserted for you: integer overflow on + - *, slice bounds on xs[i], division by zero, and narrowing casts. A recursive function carries decreases or admits divergence. Bounded quantifiers, forall i in 0..<n: P(i), are allowed in refinement positions. The verification page covers how these are discharged.