From 1915651e71ec368f8a9fd15c9bf62097a8e20145 Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Thu, 2 Jul 2026 03:34:08 +0200 Subject: [PATCH] Remove RRC_REFACTOR_READINESS.md --- docs/RRC_REFACTOR_READINESS.md | 100 --------------------------------- 1 file changed, 100 deletions(-) delete mode 100644 docs/RRC_REFACTOR_READINESS.md diff --git a/docs/RRC_REFACTOR_READINESS.md b/docs/RRC_REFACTOR_READINESS.md deleted file mode 100644 index 1835303c..00000000 --- a/docs/RRC_REFACTOR_READINESS.md +++ /dev/null @@ -1,100 +0,0 @@ -# RRC Refactor Status - -**Date:** 2026-06-21 -**Goal:** Port the Research-Stack RRC (Receipt Routing Classifier) decision surface into SilverSight. - -## Status - -**Bare-minimum refactor is complete and building.** - -- ✅ RRC logogram projection and admission gates -- ✅ Receipt core with SilverSight.Core receipt bridge -- ✅ RRC alignment gate (`determineAlignment`) + 6 canonical fixture rows -- ✅ AVM ISA (`Types`, `Value`, `Instr`, `State`, `Step`, `Run`) -- ✅ AVM canary bundle + top-level JSON emitter (`AVMIsa.Emit`) -- ✅ AVM-stamped RRC fixture corpus emitter (`emitFixtureCorpus`) -- ✅ Python raw-feature shims (`pist_matrix_builder.py`, `validate_rrc_predictions.py`) -- ✅ Executable `rrc-emit-fixture` to extract the JSON bundle -- ✅ RRC gates ported: `ReceiptDensity`, `PolyFactorIdentity`, `EntropyCandidates` -- ✅ Q16_16 cross-language roundtrip test (Lean ↔ C ↔ Python) -- ✅ Glossary entries for all new domain terms - -## Location - -The RRC layer lives under `formal/SilverSight/` (Lake module namespace `SilverSight.*`). -User-facing symlinks are in `formal/RRCLib/`. - -| File | Module | Role | -|---|---|---| -| `formal/SilverSight/RRCLogogramProjection.lean` | `SilverSight.RRCLogogramProjection` | `RRCShape`, `WitnessStatus`, projection/merge gates | -| `formal/SilverSight/ReceiptCore.lean` | `SilverSight.ReceiptCore` | `ReceiptKind`, `Receipt`, ledger, core bridge | -| `formal/SilverSight/RRC/Emit.lean` | `SilverSight.RRC.Emit` | Alignment gate, `FixtureRow`, JSON emitter | -| `formal/SilverSight/AVMIsa/Types.lean` | `SilverSight.AVMIsa` | `AvmTy` closed-world type universe | -| `formal/SilverSight/AVMIsa/Value.lean` | `SilverSight.AVMIsa` | `AvmVal` typed values | -| `formal/SilverSight/AVMIsa/Instr.lean` | `SilverSight.AVMIsa` | `Instr` / `Prim` opcodes | -| `formal/SilverSight/AVMIsa/State.lean` | `SilverSight.AVMIsa` | AVM execution state | -| `formal/SilverSight/AVMIsa/Step.lean` | `SilverSight.AVMIsa` | `step` transition function | -| `formal/SilverSight/AVMIsa/Run.lean` | `SilverSight.AVMIsa` | Fuel-bounded `run` | -| `formal/SilverSight/AVMIsa/Emit.lean` | `SilverSight.AVMIsa.Emit` | Top-level JSON output boundary | - -## Key architectural decisions - -1. **Canonical fixed point moved to Core.** - - `Core/SilverSight/FixedPoint.lean` defines `SilverSight.FixedPoint.Q16_16` / `Q0_16`. - - `formal/CoreFormalism/FixedPoint.lean` is now a compatibility shim. - - This lets `SilverSightRRC` import only `Core/` + Mathlib, preserving the library method. - -2. **Two receipt types with a bridge.** - - `Core/SilverSightCore.lean` keeps the external `Receipt` boundary. - - `formal/SilverSight/ReceiptCore.lean` adds the internal validation receipt model and a `toSilverSightReceipt` bridge. - -3. **Core AVM stays conceptual; concrete ISA lives in RRC.** - - `Core/SilverSightCore.lean` defines the abstract `δ`, `Instruction`, `AVMState` contract. - - `formal/SilverSight/AVMIsa/` implements the closed-world typed ISA. - -## Build commands - -```bash -# All libraries -lake build - -# Individual libraries -lake build SilverSightCore -lake build SilverSightFormal -lake build SilverSightRRC - -# Emit and validate the fixture corpus JSON -lake build rrc-emit-fixture -.lake/build/bin/rrc-emit-fixture > /tmp/rrc_fixture_emitted.json -python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json -``` - -## Verification results - -| Gate | Result | -|---|---| -| `lake build` | ✅ 2987 jobs, 0 errors | -| `lake build SilverSightCore` | ✅ 2987 jobs, 0 errors | -| `lake build SilverSightFormal` | ✅ 3132 jobs, 0 errors | -| `lake build SilverSightRRC` | ✅ 3006 jobs, 0 errors | -| `lake build rrc-emit-fixture` | ✅ green | -| `lake build q16-roundtrip` | ✅ 5949 jobs, 0 errors | -| `python3 -m py_compile python/pist_matrix_builder.py python/validate_rrc_predictions.py tests/test_q16_canonical.py .github/scripts/check_doc_sync.py .github/scripts/glossary_lint.py` | ✅ green | -| `python3 .github/scripts/glossary_lint.py` | ✅ no warnings | -| `python3 .github/scripts/check_doc_sync.py` | ✅ OK | -| `rrc-emit-fixture \| validate_rrc_predictions.py` | ✅ OK: 6 rows | -| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed | -| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed | -| `pytest tests/test_q16_canonical.py` | ⚠️ not run — pytest not installed in this environment | - -## Out of scope (future work) - -- Full 250-equation `Q16_16Manifold` (requires `PIST.Classify`, `PIST.Matrices250`, source JSON). -- `python/build_manifold.py` generator for the full corpus. -- PIST classifier surface to populate `pistProxyLabel` / `pistExactLabel` from real matrices. -- Concrete `WireFormat`/`LayoutBridge` instances for multi-field Core types such as `BraidState`. - -## References - -- Research-Stack sources: `0-Core-Formalism/lean/Semantics/Semantics/{RRC,AVMIsa,RRCLogogramProjection,ReceiptCore}.lean` -- SilverSight project map: `docs/PROJECT_MAP.md`