mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-18 12:10:34 +00:00
Remove TESTING.md - archived to archive/2026-07-02/docs/
This commit is contained in:
Allaun Silverfox
parent
8c520e3497
commit
ea6d22abec
1 changed files with 0 additions and 179 deletions
179
docs/TESTING.md
179
docs/TESTING.md
|
|
@ -1,179 +0,0 @@
|
||||||
# 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.
|
|
||||||
Loading…
Add table
Reference in a new issue