From 8c520e3497e74611d660b35d255b3845cc339b14 Mon Sep 17 00:00:00 2001
From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com>
Date: Thu, 2 Jul 2026 03:27:06 +0200
Subject: [PATCH] Archive TESTING.md - superseded by current state

---
 archive/2026-07-02/docs/TESTING.md | 179 +++++++++++++++++++++++++++++
 1 file changed, 179 insertions(+)
 create mode 100644 archive/2026-07-02/docs/TESTING.md

diff --git a/archive/2026-07-02/docs/TESTING.md b/archive/2026-07-02/docs/TESTING.md
new file mode 100644
index 00000000..1d91dfa3
--- /dev/null
+++ b/archive/2026-07-02/docs/TESTING.md
@@ -0,0 +1,179 @@
+# 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.