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/build_logs/2026-06-21_session_build_baseline.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

11 KiB
Raw Blame History

Build Log: 2026-06-21 — SidonSets Restoration & SilverSight Porting Graph

Session Summary

Restored CoreFormalism.SidonSets.lean to the active SilverSight build, hardened the SilverSight core surface, and generated a searchable Research Stack porting graph to guide the long-term migration of provably useful math/concepts from Research Stack.

Build Baselines

All builds run against SilverSight main at 8f1d30d with toolchain leanprover/lean4:v4.32.0-rc1.

Command Jobs Errors Notes
lake build 2978 0 Default build target
lake build SilverSightFormal 3118 0 Full formal library
lake build CoreFormalism.SidonSets 2601 0 Narrow target after restore
lake build CoreFormalism.SieveLemmas 2402 0 Ported sieve foundation
lake build CoreFormalism.InteractionGraphSidon 2530 0 Ported interaction-graph module
lake build CoreFormalism.BraidEigensolid 2680 0 Ported braid eigensolid
lake build CoreFormalism.BraidSpherionBridge 2745 0 Ported spherion bridge

What Was Ported / Restored

Core formalism modules

  • CoreFormalism.FixedPoint — canonical Q16_16 fixed-point surface
  • CoreFormalism.Tactics — common tactics for the project
  • CoreFormalism.Q16_16Numerics — numeric helpers over Q16_16
  • CoreFormalism.DynamicCanal — dynamic canal infrastructure
  • CoreFormalism.Bind — binding layer
  • CoreFormalism.BraidBracket — braid bracket primitives
  • CoreFormalism.BraidStrand — strand model
  • CoreFormalism.BraidCross — crossing model
  • CoreFormalism.BraidField — braid field operations
  • CoreFormalism.SidonSets — Sidon sets, extremal function, bounds, Singer theorem
  • CoreFormalism.SieveLemmas — sieving lemmas for Sidon constructions
  • CoreFormalism.InteractionGraphSidon — interaction graph + Sidon labeling
  • CoreFormalism.BraidEigensolid — eigensolid fixed-point theory
  • CoreFormalism.BraidSpherionBridge — braid/spherion bridge

Python tooling / tests

  • tests/test_q16_canonical.py — 10 green tests asserting canonical Q16_16 semantics
  • tests/quarantine/q16_roundtrip_test.legacy.py — archived; waits on C bridge restoration
  • .github/scripts/glossary_lint.py — warns when docs introduce undefined terms

Documentation / contracts

  • docs/GLOSSARY.md — living dictionary with standard-terminology crosswalk
  • docs/GLOSSARY_ALLOWLIST.md — allowlist for glossary lint
  • docs/TESTING.md — unit/integration/CI testing contract
  • docs/research_stack_usage_graph.{json,md,dot,svg,png} — searchable 13k-entity graph of Research Stack usage
  • docs/research_stack_porting_candidates.md — prioritized porting shortlist
  • CITATION.cff — updated with module-specific reference notes

SidonSets Restoration Details

The module was quarantined because a chaos-game appendix used invalid Lean syntax and out-of-scope identifiers. Restoration steps:

  1. Removed the broken chaos-game appendix entirely.
  2. Replaced LaTeX-style escapes (\Z, \N) with Int / Nat in comments.
  3. Introduced local abbrev Z := Int and abbrev N := Nat to avoid auto-implicit shadowing.
  4. Fixed finset decidability issues and omega/linarith failures by normalizing to Nat where appropriate.
  5. Verified with narrow and full library builds.

Research Stack Usage Graph

Generated a cross-reference graph from the Research Stack checkout at /home/allaun/Research Stack:

  • Nodes: 13 000+ files, modules, and concepts
  • Edges: 13 000+ import / usage / reference relationships
  • Outputs: JSON, Markdown, GraphViz DOT, SVG, PNG
  • Purpose: convert the legacy Research Stack into a searchable point graph so useful math, code, and goals can be located and ported deterministically.

CI / Contract Updates

  • .github/workflows/lean-check.yml — Lean build gate
  • .github/workflows/python-check.yml — Python test + glossary lint gate
  • .github/workflows/doc-sync.yml — documentation sync gate
  • docs/generate_project_map.py — regenerable project map generator

Generated Artifacts

  • docs/PROJECT_MAP.md — human-readable SilverSight project map (77 files, 10 layers)
  • docs/PROJECT_MAP.json — machine-readable project map (schema silversight_project_map_v1)

Invariants Upheld

  • No Float in any Lean compute path.
  • ofFloat only permitted at JSON/sensor boundaries.
  • Library-method architecture preserved: Core/ imports nothing; libraries import only Core/ or Mathlib; no library imports another library.
  • Q16_16 unified to CoreFormalism.FixedPoint.

Next Recommended Work

  • Restore C bridge for Q16_16 roundtrip tests.
  • Port additional Research Stack modules identified in docs/research_stack_porting_candidates.md.
  • Add #eval witnesses / roundtrip proofs for remaining core modules per docs/TESTING.md.

RRCLib Port (this session)

Ported Research-Stack RRC decision surface into SilverSight as a new library.

Files added

  • formal/SilverSight/RRCLogogramProjection.lean — RRC shape/logogram admission gates
  • formal/SilverSight/ReceiptCore.lean — receipt kinds, ledger, and toSilverSightReceipt bridge
  • formal/SilverSight/RRC/Emit.lean — 6 canonical fixture rows, alignment gate, JSON emitter
  • formal/SilverSight/AVMIsa/{Types,Value,Instr,State,Step,Run,Emit}.lean — AVM ISA + canary bundle
  • formal/RRCLib/ — user-facing symlinks to the SilverSight modules
  • exe/RrcEmitFixture.lean — executable that emits the fixture corpus JSON
  • python/pist_matrix_builder.py — PIST 8×8 matrix builder (I/O only)
  • python/validate_rrc_predictions.py — emitted JSON validator (I/O only)

Build verification

Command Jobs Errors Notes
lake build 2981 0 Default target
lake build SilverSightRRC 2992 0 New RRC library
lake build SilverSightCore 3132 0 No regression; FixedPoint now in Core
lake build SilverSightFormal 3132 0 No regression
lake build rrc-emit-fixture — 0 Executable JSON emitter

Deviations from source

  • Skipped the 250-equation corpus; added emitFixtureCorpus for the 6-row fixture corpus.
  • Moved canonical FixedPoint to Core/SilverSight/FixedPoint.lean; formal/CoreFormalism/FixedPoint.lean is a compatibility shim.
  • Actual Lean modules live under formal/SilverSight/; formal/RRCLib/ holds symlinks so the requested paths exist.

Final verification run

Gate Result
lake build ✅ 2981 jobs, 0 errors
lake build SilverSightCore ✅ 3132 jobs, 0 errors
lake build SilverSightFormal ✅ 3132 jobs, 0 errors
lake build SilverSightRRC ✅ 2992 jobs, 0 errors
lake build rrc-emit-fixture ✅ green
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
pytest tests/test_q16_canonical.py ⚠️ skipped — pytest not installed

Later same day: RRC module ports and Q16_16 cross-language roundtrip

What changed

  • Ported three Research Stack RRC gates into formal/SilverSight/RRC/:
    • ReceiptDensity.lean — Q16_16 receipt-density scoring
    • PolyFactorIdentity.lean — divisor-sum signature gate (E8Sidon surface stubbed)
    • EntropyCandidates.lean — 10 braid-state fixtures using CoreFormalism.BraidEigensolid types
  • Added a Lean ↔ C ↔ Python Q16_16 roundtrip test:
    • c/q16_canonical.c — canonical saturating Q16_16 C library
    • exe/Q16_16Roundtrip.lean — Lean executable linked via Lake extern_lib
    • tests/test_q16_roundtrip.py — Python ↔ C roundtrip harness (revived from tests/quarantine/q16_roundtrip_test.legacy.py)
  • Updated lakefile.lean with the q16-roundtrip executable and the extern_lib q16_canonical build target.

Build baselines

Command Jobs Errors Notes
lake build 2981 0 Default target
lake build SilverSightRRC 3006 0 RRC decision surface incl. new gates
lake build q16-roundtrip 5949 0 Lean ↔ C executable

Test results

Test Result
python3 tests/test_q16_roundtrip.py ✅ 21 tests passed
.lake/build/bin/q16-roundtrip ✅ 35 Lean ↔ C tests passed

Later same day: Phase 1 core — schema / layout / wireformat modules

What changed

Implemented the YaFF-inspired Phase 1 Core modules in Core/SilverSight/Semantics/:

  • Schema.lean — fixed-size schema contract (byteSize, wellFormed).
  • Layout.lean — Layout enum, AccessProfile, Q0_16 Layout.cost, chooseLayoutByCost, and an ε-suboptimality theorem.
  • WireFormat.lean — certified encoder/decoder structure (encode, decode, encode_size, roundTrip) with row-major instances for Unit, Bool, and UInt8.
  • View.lean — zero-copy view contract (base, offset, valid) and a readUInt8 accessor backed by address-arithmetic.
  • LayoutBridge.lean — certified layout conversion structure and identity bridges.
  • CanalLayout.lean — CanalRegime enum and chooseLayout override on top of the pure cost model.

Updated lakefile.lean to add all new SilverSight.Semantics.* modules to SilverSightCore. Updated docs/ARCHITECTURE.md, AGENTS.md, docs/RRC_REFACTOR_READINESS.md, and SilverSight_Spec.md to reflect the new Core surface.

Build baselines

Command Jobs Errors Notes
lake build 2987 0 Default target now includes Semantics core
lake build SilverSightCore 2987 0 Core + Semantics modules
lake build SilverSightRRC 3006 0 RRC decision surface
lake build q16-roundtrip 5949 0 Lean ↔ C executable

Verification results

Test Result
python3 tests/test_q16_roundtrip.py ✅ 21 tests passed
.lake/build/bin/q16-roundtrip ✅ 35 Lean ↔ C tests passed
python3 .github/scripts/glossary_lint.py ✅ no warnings
python3 .github/scripts/check_doc_sync.py ✅ OK

Notes

  • Semantics modules import only SilverSight.FixedPoint and Mathlib, preserving the library-method rule that Core may not depend on libraries.
  • The full DynamicCanal physics remains in CoreFormalism.DynamicCanal; CanalLayout is the Core-side abstraction that will be driven by it.
  • Concrete WireFormat/LayoutBridge instances for product types such as BraidState are left as library extensions.