# A positive affine transfer

KL-FCS-037 · Abstract interpretation · version 1.0.0

## Problem

Compute sound interval bounds for a sequence of mathematical-integer affine transforms.

## Context

Use interval summaries to enclose concrete values, and distinguish containment from exact sets.

## Definitions

- **Concrete state set**: The actual values attainable from the declared input domain.
- **Interval abstraction**: A lower and upper bound enclosing concrete values.
- **Sound transfer**: An abstract operation that contains every concrete output.

## Checked result

Sound enclosure: yes; Tight interval bounds: yes.

Endpoint propagation encloses every concrete output. Negative multiplication swaps extrema; multiple transformations compose while preserving containment.

## Checker reasoning

1. Start from every integer in the initial interval.
2. Apply each affine transform to the concrete set.
3. Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.
4. Check every concrete value remains enclosed and the final bounds are tight.

## Dataset construction

{
  "family": "abstract-interpretation",
  "task": "Compute sound interval bounds for a sequence of mathematical-integer affine transforms.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete concrete inputs + interval transfer replay",
  "acceptance": [
    "Start from every integer in the initial interval.",
    "Apply each affine transform to the concrete set.",
    "Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.",
    "Check every concrete value remains enclosed and the final bounds are tight."
  ],
  "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": {
    "initial_interval": [
      -2,
      3
    ],
    "transforms": [
      [
        2,
        1
      ]
    ]
  },
  "claim": {
    "sound": true,
    "tight_interval": true
  },
  "witness": {
    "intervals": [
      [
        -2,
        3
      ],
      [
        -3,
        7
      ]
    ]
  }
}
```

## Complexity

With a concrete interval of k integers and t transformations, this finite replay costs O(kt). Abstract endpoint propagation alone costs O(t).

## Limits

The abstraction encloses gaps. Machine overflow, branches, and widening are not modeled.

## Common error and further work

A tight interval can include unattainable interior values; it is not necessarily an exact concrete set.

Add control-flow joins, fixed points, widening, and overflow-specific abstractions.

## Verification

Complete concrete inputs + interval transfer replay. 6 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://www.di.ens.fr/~cousot/AI/)