mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
40e223fdd9
Five new formal modules, all clean rewrites (not ports from Research Stack). Based on the chiral CRT multiplexing framework. 1. HCMR.lean (Hardware Contention Markov Representation) - Self-loop probs: SUBLEQ=0.823, AVX-512=0.885, ring=0.0 - Throughput = base_rate × (1 - self_loop_prob) - Theorems: ring > SUBLEQ > AVX-512 ordering, COUCH stability - Connection: self_loop = Sidon collision rate 2. CacheSieve.lean (L0 Local Sorter Cache Admission) - 4-state machine: Stable → Rising → Unstable → Reset - Admission control + victim selection - Theorems: stable→promote, high contention→demote, COUCH evicts - Connection: COUCH gate = contention threshold filter 3. Blitter6502OISC.lean (6502 OISC Blitter) - SUBLEQ instruction semantics: M[b] := M[b] - M[a] - Blitter: 3 SUBLEQ per byte (negation trick) - Theorems: subtract semantics, branch on ≤0, ring faster than SUBLEQ - Connection: blitter is the 'word SUBLEQ' regime from HCMR 4. YangMillsPerformance.lean (Distributed Performance) - 5 layers: cache → memory → sync → compression → network - Composed throughput = base × ∏(1 - overhead_i) - Theorems: cache highest overhead, more layers = less throughput - Connection: cache overhead = HCMR SUBLEQ self-loop 5. WorkloadTestbench.lean (Virtual GPU Workload Simulation) - 5 workload types: stream, strided, random, gather, scatter - Maps workloads to HCMR ops and CacheSieve states - Theorems: stream highest throughput, random causes Reset - Connection: stream = ring dispatch, random = AVX-512 Suite composition: WorkloadTestbench (workload → op type) → HCMR (op → self-loop → throughput) → CacheSieve (contention → admit/evict) → Blitter6502OISC (concrete SUBLEQ execution) → YangMillsPerformance (distributed stack composition) All modules registered in lakefile.lean as SilverSightRRC roots. Lean v4.30.0-rc2, Mathlib dependency. Known sorries: 2 (CacheSieve.evict_prefers_reset needs List API work, YangMillsPerformance.compression_overhead_bounded needs conservation law formalization). All other theorems are complete. |
||
|---|---|---|
| .. | ||
| AVMIsa | ||
| CollectiveIntelligence | ||
| FeasibleSet | ||
| PIST | ||
| RRC | ||
| AdjugateMatrix.lean | ||
| AngrySphinx.lean | ||
| Blitter6502OISC.lean | ||
| CacheSieve.lean | ||
| ColdReviewer.lean | ||
| CollatzBraid.lean | ||
| FixedPointBridge.lean | ||
| GCCL.lean | ||
| GoldenSpiral.lean | ||
| HachimojiCharClass.lean | ||
| HachimojiN8.lean | ||
| HachimojiN8Bridge.lean | ||
| HCMR.lean | ||
| PhiConsistency.lean | ||
| PhiDNALayout.lean | ||
| PhiPipelineReceipt.lean | ||
| PrimeLut.lean | ||
| ProductSchema.lean | ||
| ProductWireFormat.lean | ||
| Receipt.lean | ||
| ReceiptCore.lean | ||
| RollupEvent.lean | ||
| RRCLogogramProjection.lean | ||
| Schema.lean | ||
| WireFormat.lean | ||
| WorkloadTestbench.lean | ||
| YangMillsPerformance.lean | ||