# Design and compatibility semantics

## 1. Design goal

EvoWitness answers a set-inclusion question. For a contract `C`, let `Accept(C, T)` be the set of JSON values accepted by object type `T`.

- backward compatibility requires `Accept(old, T) ⊆ Accept(new, T)`;
- forward compatibility requires `Accept(new, T) ⊆ Accept(old, T)`;
- full compatibility requires both inclusions.

The analyzer does not enumerate these infinite sets. It decomposes inclusion into local rules whose counterexamples can be constructed deterministically.

## 2. Pipeline

```mermaid
flowchart LR
  A["Old DSL"] --> P1["Parser"]
  B["New DSL"] --> P2["Parser"]
  P1 --> M1["Contract model"]
  P2 --> M2["Contract model"]
  M1 --> R["Directional rule engine"]
  M2 --> R
  R --> W["Witness constructor"]
  W --> V["Dual-contract validator"]
  V --> O["Markdown / JSON / SARIF / witness pack"]
```

Each parser produces immutable public models and stable diagnostics. The rule engine always receives a data-producing source contract and a receiving target contract; forward mode simply reverses this flow. This keeps every local rule expressed as “does target accept every source value?”

## 3. Rule families

### Object rules

- source type absent from target → breaking;
- source object open and target closed → breaking, witnessed by `__extra`;
- source closed and target open → safe widening;
- target-only type → safe for this data direction.

### Field rules

- source field absent from closed target → breaking;
- source field absent from open target → accepted but reported informationally;
- target-only required field → breaking, witnessed by omission;
- target-only optional field → safe;
- optional source field becoming required → breaking.

### Type rules

Types are compared by accepted-value inclusion, not spelling alone. `int → number` is widening; the reverse rejects fractional values. Enum target values must be a superset of source values. References and list item types currently require stable names.

### Constraint rules

A target minimum must be no greater than the source minimum. A target maximum must be no smaller than the source maximum. `None` represents an unbounded side. String and list lengths follow the same order.

## 4. Witness construction

A witness is a JSON payload with four properties:

1. it is syntactically valid JSON;
2. it satisfies all required fields in the source object;
3. it selects a value immediately outside the target's narrowed set;
4. it avoids unrelated optional data.

Examples:

- newly required field: omit that field;
- enum value removed: choose the first removed value;
- minimum raised from 0 to 5: choose 0;
- unbounded minimum changed to 5: choose 4;
- maximum lowered to 80: choose 81;
- minimum length raised from 1 to 8: choose a one-character string;
- object closed: add `"__extra": null`.

Required referenced objects are built recursively. A visited-type set and depth cap stop recursive contracts, producing `{}` at the cycle boundary. This is sufficient for the outer structural witness, while the verifier reports if an inner recursive requirement makes a finite witness impossible.

## 5. Verification

`verify_witness` parses the generated payload once for each contract, runs the same public instance validator, and returns source/target validity plus path-addressed issues. Core tests require every representative backward witness to be source-valid and target-invalid.

The validator checks:

- object shape and closed-object extras;
- required fields;
- string, integer, number, boolean and enum types;
- numeric and length bounds;
- nested references;
- list length and item types.

## 6. Determinism

Object and field traversal preserves declaration order. Rule codes, paths and witness selection are stable. Reports contain no timestamps, random values or platform-dependent paths, so identical inputs produce byte-identical JSON, SARIF and witness packs.

Witness case ids combine report order, rule code and path. They are not content hashes; they are review-stable names for the deterministic local ordering used by the analyzer.

## 7. Complexity

The current lookup model uses ordered arrays. With `O` objects and up to `F` fields per object, a directional comparison is `O(O² + O·F²)` in the worst case. Contract documents are normally small, and ordered arrays guarantee deterministic output. A future index can reduce lookup cost without changing public semantics.

Instance validation is linear in the visited JSON members and declared fields, excluding repeated linear name lookup. Recursive validation follows the finite payload tree rather than the potentially cyclic schema graph.

## 8. Explicit boundaries

Version 0.1.0 does not claim full JSON Schema compatibility, regex analysis, union-type subtyping, satisfiability solving, registry governance or JUnit-style release evidence. Those features require different project boundaries. Keeping the first release's constraint algebra closed and constructive ensures every breaking rule has a clear, testable counterexample.