package corrected

// FirstNegative returns the first negative index, or len(items).
// Authored teaching contract: len(items) <= 32; input is not mutated.
//
// reqproof:requires 0 <= len(items) && len(items) <= 32
//
//	reqproof:lemma scan_contract func(items []int) bool {
//	  result := FirstNegative(items)
//	  return 0 <= result && result <= len(items) && PrefixOK(result, items) && (result == len(items) || items[result] < 0)
//	}
//
//go:noinline
func FirstNegative(items []int) int {
	i := 0
	// reqproof:invariant 0 <= i && i <= len(items)
	// reqproof:invariant PrefixOK(i, items)
	for i < len(items) && items[i] >= 0 {
		i++
	}
	return i
}

// PrefixOK is a recursive expression of the completed-prefix claim.
// Its call precondition is 0 <= end <= len(items) <= 32.
// The decreases directive is syntactic support, not a solver-proved
// total-correctness guarantee. No element arithmetic is performed.
//
// reqproof:requires 0 <= end && end <= len(items) && len(items) <= 32
// reqproof:decreases end
func PrefixOK(end int, items []int) bool {
	if end <= 0 {
		return true
	}
	return items[end-1] >= 0 && PrefixOK(end-1, items)
}