# SilverSight Testing Rules

Testing is not an afterthought.  Every module that claims a property must
provide a way to witness that property — at minimum a `#eval` witness for Lean
and a unit test for Python.  This document defines the rules before the project
outgrows them.

---

## 1. Philosophy

- **A theorem without a witness is a draft.**  Lean proofs are required for
  gates; `#eval` witnesses are required for computable claims.
- **A shim without a unit test is untrusted.**  Every Python module that
  performs I/O, parsing, or feature extraction must have matching unit tests.
- **A receipt without a roundtrip is incomplete.**  Any receipt format must be
  serializable, deserializable, and byte-identical on the roundtrip.
- **A new term without a glossary entry is undocumented.**  The glossary lint
  (`python3 .github/scripts/glossary_lint.py`) must stay green.

---

## 2. Lean tests

### Location and naming

```text
formal/CoreFormalism/Foo.lean        ← implementation
formal/CoreFormalism/Foo/Test.lean   ← Lean tests for Foo (when test count grows)
tests/lean/FooTest.lean              ← alternatively, a central tests/lean tree
```

For small modules, tests may live at the bottom of the implementation file as
`#eval` witnesses.  When a module exceeds ~500 lines or has more than five
witnesses, split tests into a separate `Test.lean` file.

### Required witnesses

Every Lean module in the active build must include at least one of the
following:

1. **Type-correctness smoke test** — `#check` the main definition.
2. **Computational witness** — `#eval` showing the definition produces the
   expected value on a concrete input.
3. **Property witness** — a short `example` block proving a trivial but
   representative instance of the main theorem.
4. **Roundtrip witness** — for any encoder/decoder pair, prove or `#eval`
   `decode (encode x) = x` on a concrete `x`.

### Anti-patterns

- Do not rely on `sorry` or `admit` in committed code.  CI rejects them.
- Do not put long-running `#eval` witnesses in files built by default unless they
  are necessary for the proof story.
- Do not import test files into production modules.

### Running Lean tests

```bash
# Build the whole formal library
lake build SilverSightFormal

# Build a specific module and its witnesses
lake build CoreFormalism.FixedPoint

# Check for sorries/admits in formal code
rg "sorry|admit" formal/ Core/
```

---

## 3. Python tests

### Location and naming

```text
python/foo.py           ← implementation
tests/test_foo.py       ← pytest unit tests
qubo/bar.py             ← implementation
tests/test_bar.py       ← pytest unit tests
```

Use the `tests/` directory for all Python tests.  Mirror the module path when
possible: `python/chaos_game.py` → `tests/test_chaos_game.py`.

### Required tests

Every Python module must have tests covering:

1. **Happy path** — typical input produces expected output.
2. **Boundary** — empty input, zero, maximum, or minimum values.
3. **Error path** — malformed input raises the documented exception.
4. **No-Float drift** — any function that returns a fixed-point value must
   roundtrip through the canonical Q16_16 representation without loss.

### Example

```python
# tests/test_q16_canonical.py
from python.q16_canonical import q16_from_float, q16_to_float

def test_q16_roundtrip():
    for x in [0.0, 1.0, -1.0, 3.1415926535, -65535.999]:
        raw = q16_from_float(x)
        assert abs(q16_to_float(raw) - x) < 1.5e-5
```

### Running Python tests

```bash
pytest tests/ -v
python3 -m py_compile python/*.py qubo/*.py
```

---

## 4. Integration tests

Integration tests live in `tests/integration/` and exercise end-to-end flows:

- `test_receipt_roundtrip.py` — generate a receipt, serialize to JSON,
  deserialize, verify equality.
- `test_chaos_to_q16.py` — run the chaos game, produce addresses, and assert
  they are valid Sidon labels.
- `test_finsler_qubo.py` — build a Finsler metric, convert to QUBO, solve, and
  check that the returned path is feasible.

Integration tests may be slow; CI runs them but they are allowed to be skipped
locally with `pytest -m 'not slow'`.

---

## 5. Documentation tests

Documentation is part of the contract and is tested:

- **Glossary lint** — warns when a domain term appears repeatedly in docs but is
  not defined in `docs/GLOSSARY.md`.
  ```bash
  python3 .github/scripts/glossary_lint.py
  ```
- **CFF validation** — `CITATION.cff` must remain valid YAML.
  ```bash
  python3 -c "import yaml; yaml.safe_load(open('CITATION.cff'))"
  ```
- **Doc sync check** — README, PORTING_MAP, and AGENTS must mention every
  top-level directory.
  ```bash
  python3 .github/scripts/check_doc_sync.py
  ```

---

## 6. CI gates

Every push and pull request must pass:

1. `lake build` — default target builds.
2. `lake build SilverSightFormal` — formal library builds.
3. `pytest tests/ -v` — Python tests pass.
4. `python3 -m py_compile` on touched `.py` files.
5. `python3 .github/scripts/glossary_lint.py` — no undefined repeated terms.
6. `python3 .github/scripts/check_doc_sync.py` — README matches tree.
7. `rg "sorry|admit" formal/ Core/` — no committed placeholders.
8. `python3 -c "import yaml; yaml.safe_load(open('CITATION.cff'))"` — CFF valid.

---

## 7. Test-driven porting checklist

When porting a Research Stack module to SilverSight:

- [ ] Module builds (`lake build CoreFormalism.X`).
- [ ] No `sorry` or `admit` in the ported surface.
- [ ] At least one `#eval` witness or `example` block added.
- [ ] Python shim (if any) has a matching unit test.
- [ ] New terms added to `docs/GLOSSARY.md` or `docs/GLOSSARY_ALLOWLIST.md`.
- [ ] `PORTING_MAP.md` status updated.
- [ ] `AGENTS.md` updated if boundaries changed.