From 231ea2abd2adcb589a01f5442097c6eabe939ff0 Mon Sep 17 00:00:00 2001 From: allaun Date: Wed, 1 Jul 2026 01:07:09 -0500 Subject: [PATCH] refactor(lean): replace native_decide with simp in HardwareContentionMarkov 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) --- .../SilverSight/HardwareContentionMarkov.lean | 24 +++++++++++++------ 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean index 2afe5b62..50f08a26 100644 --- a/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean @@ -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