package weak

// 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_bounds func(items []int) bool {
//	  result := FirstNegative(items)
//	  return 0 <= result && result <= len(items)
//	}
//
//go:noinline
func FirstNegative(items []int) int {
	i := 0
	if len(items) > 0 {
		i = 1
	}
	// reqproof:invariant 0 <= i && i <= len(items)
	for i < len(items) && items[i] >= 0 {
		i++
	}
	return i
}