# Insertion sort over a finite domain

KL-FCS-001 · Algorithms · version 1.0.0

## Problem

Sort every list of length 0–5 over {−1, 0, 1}, preserving every occurrence.

## Context

Separate a program’s behavior from its specification. Exhaustive finite domains expose ordering, multiplicity, empty-input, and duplicate-value errors.

## Definitions

- **Input contract**: A precise set of admissible inputs, including sizes and value ranges.
- **Postcondition**: The relation between the original input and the returned output.
- **Oracle**: A separately implemented reference property used to accept or reject a candidate.

## Checked result

Correct over the stated input domain: yes.

The candidate shifts larger values to the right before inserting the next value. A separate checker compares every declared input with Python’s reference ordering. Duplicates and the empty list are included.

## Checker reasoning

1. Enumerate every list in the declared alphabet and length bound.
2. Run the candidate insertion-sort implementation without modifying the source input.
3. Compare each result with the reference ordering, including repeated elements.
4. Reject immediately with an input witness if ordering or multiplicity differs.

## Dataset construction

{
  "family": "algorithms",
  "task": "Sort every list of length 0–5 over {−1, 0, 1}, preserving every occurrence.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Exhaustive bounded validation · 364 inputs",
  "acceptance": [
    "Enumerate every list in the declared alphabet and length bound.",
    "Run the candidate insertion-sort implementation without modifying the source input.",
    "Compare each result with the reference ordering, including repeated elements.",
    "Reject immediately with an input witness if ordering or multiplicity differs."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "alphabet": [
      -1,
      0,
      1
    ],
    "max_length": 5
  },
  "claim": {
    "correct_on_declared_domain": true
  },
  "witness": {
    "function": "insertion_sort"
  }
}
```

## Complexity

For alphabet size k and maximum length n, this family checks Σ kⁱ inputs for i=0…n. Insertion sort performs O(n²) comparisons in its worst case.

## Limits

This is not a general proof for arbitrary lists, a stability proof, or a complexity result.

## Common error and further work

Sortedness alone does not prove that an output preserves the input multiset.

Add stability certificates for tagged records or an unbounded inductive invariant.

## Verification

Exhaustive bounded validation · 364 inputs. 364 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://ocw.mit.edu/courses/6-006-introduction-to-algorithms-fall-2011/)