allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(lean): replace native_decide with simp in HardwareContentionMarkov

Browse source 
All  theorems replaced with:
  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]

Also added no-native-decide-no-float skill at ~/.opencode/skills/ to
enforce the research stack rules on every turn.
Build: 3308 jobs, 0 errors (lake build SilverSight)
This commit is contained in:
allaun 2026-07-01 01:07:09 -05:00
parent f346cf55d1
commit 231ea2abd2
1 changed files with 17 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean
View file

@ -53,23 +53,29 @@ def measuredRingRate : Q16_16 := Q16_16.ofRatio 105127 100
/-- Self-loop ordering: SUBLEQ has more contention than ring. -/
theorem subleq_contention_gt_ring : subleqSelfLoop.val >= ringSelfLoop.val := by
native_decide
unfold subleqSelfLoop ringSelfLoop Q16_16.ofRatio Q16_16.zero
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
/-- Self-loop ordering: CL has more contention than SUBLEQ. -/
theorem cl_contention_gt_subleq : clSelfLoop.val >= subleqSelfLoop.val := by
native_decide
unfold clSelfLoop subleqSelfLoop Q16_16.ofRatio
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
/-- Mixing model: ringRate equals measuredRingRate exactly. -/
theorem ring_rate_match : ringRate.val = measuredRingRate.val := by
native_decide
unfold ringRate measuredRingRate baseRate mixingRate ringSelfLoop
unfold Q16_16.ofRatio Q16_16.zero Q16_16.one Q16_16.sub Q16_16.mul
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
/-- Throughput ordering: ring is fastest. -/
theorem ring_fastest : measuredRingRate.val >= measuredWordRate.val := by
native_decide
unfold measuredRingRate measuredWordRate Q16_16.ofRatio
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
/-- Throughput ordering: word is faster than CL. -/
theorem word_faster_than_cl : measuredWordRate.val >= measuredClRate.val := by
native_decide
unfold measuredWordRate measuredClRate Q16_16.ofRatio
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
/--
Cache tunnel miss probability per instruction.
@ -96,10 +102,14 @@ Applying throughput_antitone to our three chains:
ringRate >= wordRate >= clRate
-/
theorem ring_rate_gte_word : ringRate.val >= wordRate.val := by
native_decide
unfold ringRate wordRate baseRate mixingRate ringSelfLoop subleqSelfLoop
unfold Q16_16.ofRatio Q16_16.zero Q16_16.one Q16_16.sub Q16_16.mul
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
theorem word_rate_gte_cl : wordRate.val >= clRate.val := by
native_decide
unfold wordRate clRate baseRate mixingRate subleqSelfLoop clSelfLoop
unfold Q16_16.ofRatio Q16_16.one Q16_16.sub Q16_16.mul
simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
#eval subleqSelfLoop
#eval mixingRate baseRate subleqSelfLoop