# Loop invariant: a first-negative scan

This kit deliberately distinguishes a correct result on selected examples from an actual source-verifier result. It is original fictional teaching work, not a production incident or customer-approved policy. Read CONTRACT.md and PROVENANCE.json first.

The operation accepts Go []int of length0..32, including nil and nonnil-empty, with arbitrary Go int element values. Return the first negative element's index, otherwise len(items). Preserve every input value and nilness. The length bound is a caller precondition; no runtime validator or error return is provided.

## Actual primary observations

One Oct28UTC campaign used Go1.26.3 darwin/arm64, a fresh current-worktree Proof executable, and Z34.15.4. The source build revision is b566a01085f0233c0be2c71508a2d3caac0cf47a; the tracked tree was dirty with site/research work, but no tracked Go/go.mod/go.sum source difference was reported. The exact build SHA, selected-source fingerprint, dependency fingerprint, argv/buildinfo and raw outcomes are retained. The previously installed Proof binary was not used. No network or solver download was requested.

| Source variant | Finite literal cases | Actual source-verifier result |
|---|---:|---|
| baseline: starts at1 when nonempty |6/7|scan_contract TIMEOUT after15s, exit1|
| corrected: starts at0 |7/7|scan_contract TIMEOUT after15s, exit1|
| weak: baseline body, bounds-only invariant and goal |6/7|scan_bounds PROVED, exit0|

All three actual source results contain exactly one lemma and an emitted query that calls the translated FirstNegative host/loop. No cache hit or unsupported fallback marker was observed. The weak result is a valid result for a weaker mathematical claim; it does not prove the first-negative contract. Both strong contracts remain unproved, not disproved by the solver. No solver counterexample was obtained. No solver retry was run to force a green result.

The decisive literal case is input[-1,2]: expected index0, baseline and weak return2, corrected returns0. Cases cover nil, empty, negative-first/middle/last, zero-only and all-nonnegative. These are seven representations but six distinct element sequences because nil and empty share the empty sequence. There are21 recorded operation callsite/return observations, not21 independent properties or exhaustive input coverage. The literal Python oracle does not derive the expected index from PrefixOK or a scan. It checks exact integer type plus all input values and nilness. All21 selected input snapshots are preserved.

Compiler count coverage was attempted but unavailable: the output directory and exported coverage.txt are empty, with the retained warning “no applicable files found in input directories.” Exit0 from that export is not coverage evidence. The original observer's method label incorrectly described intended coverage as achieved. Its complete original source and raw stdout remain under observed/. The public observer changes ONLY that metadata string to a truthful callsite/result description; see OBSERVER-METADATA-AMENDMENT.json and the exact patch. That metadata-corrected public observer was not primary-executed after the correction. No independent entry-counter, profiling or branch-coverage claim is made.

## Portable runtime replay

Prerequisites: normal CPython3.12+ and Go1.26.3+ already installed. No pip, Proof, Z3 or network is needed for this path; Go module has no external dependencies. The script disables module downloads and refuses an existing output directory.

    python3 -B reproduce.py --output /tmp/loop-invariant-new-run

It builds and calls the actual three supplied Go implementations, then applies the independent literal oracle. The new output has its own runtime, commands, hashes and date. Exit0 means the expected finite defect/correction/weak-source contrasts reproduced. It does not accept either faulty variant or prove the strong contract. This public replay intentionally does not promise compiler coverage instrumentation.

## Two distinct optional proof paths

With an already installed Z3:

    python3 -B reproduce.py --output /tmp/loop-invariant-query-replay --replay-smt --z3 /path/to/z3

This also replays the exact retained SMT files with a15second process budget. It is a new solver/query replay, not a new translation of Go, and solver results can differ by version/resources. Retain the returned output; TIMEOUT/UNKNOWN/unsupported is not PROVED. The raw retained queries include get-model, so UNSAT followed by a model-unavailable message is not a counterexample.

With an existing Proof executable built from the source/version you intend to assess, and its configured Z3:

    python3 -B reproduce.py --output /tmp/loop-invariant-source-replay --proof /path/to/proof

This runs the actual supported verify-lemma command on all three packages with --solver z3 --no-download --no-cache --format json --show-query --timeout15s (the argv spells timeout and15s as separate arguments). It records that caller-supplied binary's hash and actual nonempty per-lemma verdicts. The primary158MB Proof binary/current repository is not bundled; do not pretend the new binary is the archived build. Proof may require a separately installed configured solver. A zero-lemma or --allow-unknown CLI policy is not an acceptance gate; this script does not use --allow-unknown.

## Reasoning boundaries

At entry, index0 establishes an empty accepted prefix. An iteration checks the current sign before incrementing. At ordinary guard-false exit, the prefix plus negative-or-end establishes the first-negative result. Bounds alone establish none of the prefix contents. The original source contains no break/early-return loop exit, so do not broaden this argument to those exits.

The separate termination argument is mathematical: len(items)-i is nonnegative and decreases by1 on each loop iteration; PrefixOK reduces end to0. Current Proof's decreases path is best-effort syntactic checking, not a total-correctness certificate. Go integer widths become unbounded SMT Int; the example avoids arithmetic on element values, and its index/end arithmetic stays0..32 under the authored preconditions. This explicit correspondence is not general Go overflow safety.

The wrapper's len<=32 assertion is visible, but the emitted quantified loop obligations range over arbitrary Seq Int states. This is not bounded loop unrolling, and no cause for the timeouts is established. The SMT result lemma contains neither an input-frame clause nor nilness; Seq Int does not distinguish nil from empty. Frame/nilness observations are finite runtime evidence, with additional manual read-only source review. No caller integration, all-length closure, concurrency, persistence, resource failure, customer approval or accepted Change/release is claimed.

## Integrity

SHA256SUMS covers all other portable members including MANIFEST.json; MANIFEST.json covers the non-manifest/checksum members. The outer ZIP checksum is published beside the download, avoiding recursive manifests. observed/ contains actual primary stdout/stderr, queries, commands and the original observer. PROVENANCE.json identifies actual versus metadata-corrected source and every unresolved limit. No private customer data or credentials are included.