這是最貼近金屬的領域。
最終生成的二進位制指令序列，必須能夠逆向回連到上層語義。
無論是高效率的條件傳送cmov、向量混合blend，還是用於打包求最小值的pminsd，甚至是幾條為了避開流水線冒險而看似繞遠路的邏輯指令組合，都必須由系統自動給出嚴格的邏輯等價證明。
裴礪在辦公室裡那個關於規模化的刁鑽問題，首到這一年，才在廢土的黃沙中，得到了江臨用程式碼堆砌出的工程回答。
零一驗證器從來都不是終點，它不過是一條通向微核心工業化的堅固證明鏈的第一環。
第十九年，江臨迎來了另一個巨大的挑戰。
代價評估後端重寫。
舊版本的代價模型天真得可笑，它只會根據靜態的指令週期給出一個冰冷的排名。
第一名，理論上看起來最快。
第二名，看起來慢一點。
但在真實的馮·諾依曼架構機器上，矽片不是乾淨的數學紙面，它充滿了物理世界的狂躁與不確定。
L1/L2快取命中率會隨著上下文波動。
作業系統的執行緒排程會隨時引發中斷。
CPU的睿頻機制會因為熱量的累積而動態改變工作頻率。
不同的處理批次大小會徹底改變流水線的吞吐瓶頸。
同樣一段看似完美的指令，在機器A上巧妙地避開了執行埠的擁堵，到了機器B上，可能正好一頭撞進分支預測器失誤的懲罰陷阱中。
所以，江臨徹底推翻了舊後端。
新後端不再輸出蒼白無力的單點分數。
對於每一個候選的微核心，它輸出的是三組立體的評估。
理論代價： 基於微架構模型的純靜態計算。
實測分佈： 候選微核心必須在多種快取冷熱狀態、多種批次長度、多種程式碼預熱方式、甚至多種強制鎖頻條件下，進行數萬次的重複測試，繪製出執行時間的機率密度分佈圖。
魯棒性評分： 衡量程式碼在惡劣硬體噪聲下的抗干擾能力。
最終被MPS-Kernel保留下來的，絕對不是某一次特定Benchmark跑分中僥倖跑出的冠軍。
而是在排除了所有硬體環境噪聲視窗之後，其效能底線依然能夠穩定領先其他方案的鐵血候選者。
第二十西年，工作站風扇發出一陣持續的嘶吼，MPS-Kernel終於生成了第一批真正意義上的證據卡。
每一張證據卡，都對應著一個經過千錘百煉的微核心包。
這不再是一段冷冰冰的程式碼，而是一段程式碼無可辯駁的履歷檔案。
【Kernel_ID: Median9_Zen3_Opt】
】一歸則規告宣按0-/0+，沉下一統NaN， kaew tcirts :scitnameS_tcartsbA【
】過證驗構同RI，位溢BU無 :foorP_RI_ecruoS【
】TASNU尋搜例反TMS，域義語告宣在 :ecnelaviuqE_yraniB【
】件套充擴2XVA ，46-68x :ASI【
】線曲級降取快冷附另；徑路取快熱D1L :noitpmussA_erutcetihcraorciM【
】告報析分時延爭競埠 :ledo【
】圖本樣尾長與99P/59P/05P、佈分遲延 :noitubirtsiD_kramhcneB【
】定穩界下能效窗視本樣%9.99 :erocS_ssentsuboR【
】徑路退回級降量標的時效失XVA當 :htaP_kcabllaF【
。本版2.0v了到進推鏈工的大龐個整將臨江，年一十三第
。題問k-pot的下景場限齊對憶記定特在及以，9naidem、8knar、8tros：心核小的界邊5tros了越遠遠批一理地定穩其極夠能經己它
。界邊的示演場那室公辦越夠足們它但，大龐算不然依中程工代現的行萬百數輒在西東些這
。景盆的構結學數亮漂示展上題問玩種這5tros在能隻是不絕lenreK-SPM，了明證界世向它
。力潛的軍進工心核微級業工產生化自正真著向，型模價代棒魯度維多和鏈明證輯邏層三，尋搜類價等義語著沿了備經己它
。稿定的圖張二第了下畫臨江，年五十三第土廢
】端後價代棒魯—鏈帶攜明證—尋搜類價等義語：2.0v lenreK-SPM【：題標
。殺大個一是會將這
