# FirstNegative teaching contract

This is a newly authored fictional requirement, not a customer-approved production specification. The incoming domain is Go `[]int`, including nil and nonnil empty slices, with length at most32. This length bound is a caller precondition; the implementation does not validate it. Elements may have any Go int value. A negative element is ordinary data, not an error return.

Return the smallest index whose element is negative; if none is negative, return len(items). Do not change any input element, length or nilness. There is one integer result and no error result. No I/O, shared state, allocation guarantee, concurrency or caller integration is claimed.

The independent literal cases in cases.json were written before execution. The Python acceptance oracle must compare exact integer outcomes and complete input snapshots including nilness; it must not compute expected indices using PrefixOK or a scan implementation. Nil and empty are two representations, both index0, not two different element sequences.

At the scan loop head,0<=i<=len(items) and every item before i is nonnegative. PrefixOK(end,items) expresses that completed-prefix property recursively under0<=end<=len(items)<=32. At entry i=0 the prefix is empty. One iteration advances only after items[i]>=0; that extends the property by one element. At exit, the condition is false: either i=len(items), or items[i]<0; with the prefix property this is the first negative item. Bounds alone do not establish the contents of the completed prefix.

The baseline deliberately begins at1 for nonempty input (0 for empty), skipping the first check. The correction starts at0. The weak source retains the faulty initialization but removes the prefix invariant and changes the lemma to returned-index bounds only. A PROVED verdict for that weaker claim, if observed, must not be described as a proof of the first-negative contract.

Termination is a separate mathematical argument: len(items)-i is nonnegative and decreases by1 in each iteration. PrefixOK decreases end by1 to0. The current decreases annotation path has only best-effort syntactic validation; annotations alone do not prove total correctness. Runtime finite completion does not prove universal termination. The current translator maps Go integer widths to SMT unbounded Int. This example compares values without arithmetic and confines index increments/decrements to0..32 under its stated preconditions, so the arithmetic correspondence is reasoned explicitly; it is not a general Go overflow result.

Proof must actually translate the intended FirstNegative host, emit its loop obligations and call-dependent lemma, and return a nonempty per-lemma result. Keep SMT query, assumptions, diagnostics, fallback markers, cache metadata and solver verdict separately from finite Go observations. Unknown/timeout/unsupported is not PROVED, and CLI exit0 alone can also mean zero lemmas. No changes to Proof or solver are part of this experiment.