allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/docs/RRC_REFACTOR_READINESS.md
allaun 3504bca392 feat(lean): add SilverSight Semantics core modules (Schema, Layout, WireFormat, View, LayoutBridge, CanalLayout) 
Implements the YaFF-inspired separation of schema, layout, and access pattern
in Core/SilverSight/Semantics/:

- Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed.
- Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector
  with an ε-suboptimality theorem.
- WireFormat.lean: certified encode/decode/roundTrip/encode_size structure.
- View.lean: zero-copy View with address-arithmetic invariant.
- LayoutBridge.lean: certified layout-conversion structure and identity bridges.
- CanalLayout.lean: CanalRegime enum and regime-aware layout selection.

Also updates:
- lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore.
- docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json},
  build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md.
- AGENTS.md: build baseline, blessed surfaces, and pending proof work.

Build: 2987 jobs, 0 errors (lake build)
Tests: Python 21/21, Lean/C 35/35
2026-06-21 14:00:56 -05:00

4.8 KiB
Raw Blame History

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

# 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 Corpus250 (requires PIST.Classify, PIST.Matrices250, source JSON).
  • python/build_corpus250.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