From ea6d22abec0945b275e2f3d565ddb026c9523f4d Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Thu, 2 Jul 2026 03:27:50 +0200 Subject: [PATCH] Remove TESTING.md - archived to archive/2026-07-02/docs/ --- docs/TESTING.md | 179 ------------------------------------------------ 1 file changed, 179 deletions(-) delete mode 100644 docs/TESTING.md diff --git a/docs/TESTING.md b/docs/TESTING.md deleted file mode 100644 index 1d91dfa3..00000000 --- a/docs/TESTING.md +++ /dev/null @@ -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.