第二張圖，是MPS-Kernelv0.2的工具鏈圖。
關於軟體與底層微核心的博弈，是從廢土第五年正式打響的。
江臨沒有再碰sort5。
那個問題己經在陳啟明的辦公室裡演示過。
辦公室那半個小時的驚豔，解決的僅僅是學術界最基礎的問題：“這條路在理論上能不能走通？”
第九次廢土要解決的，是：“這套系統，到底能不能放大？”
現實總是毫不留情。
第一版試圖規模化的搜尋器，在第六年迎來了轟轟烈烈的全面崩潰。
系統崩潰的原因，並非零一驗證器證明速度太慢，也不是他建立的硬體代價模型不夠精確。
而是候選指令還沒有來得及排隊進入驗證器，前端的生成器就己經因為組合爆炸，將狀態空間膨脹到了一個工作站記憶體根本無法承受的黑洞級別。
sort8還能靠著壓榨交換檔案的I/O勉強跑完。
可一旦觸及median9，狀態樹就開始扭曲變形。
等他試著展開一個哪怕附加了限制條件的top-k小核心時，生成器吐出的垃圾候選程式碼在幾個小時內把幾塊TB級企業硬碟徹底寫滿，交換分割槽被打穿，日誌系統開始報錯，最終程序被OOM killer殺掉，工作站在持續I/O雪崩中卡死。
這次失敗，不僅沒有讓江臨沮喪，反而讓他感到興奮。
裴礪的判斷是精準的。
真正擋在MPS-Kernel前面的，不是某一段晦澀難懂的程式碼，而是不可阻擋的數學規律。
狀態空間爆炸。
第八年，江臨果斷在程式碼庫中按下刪除鍵，將列舉指令序列這條傳統的暴力窮舉舊路線抹除。
搜尋的核心物件，被他從具體的程式碼改成了抽象的語義等價類。
不再讓生成器像個傻子一樣去列舉每一種可能的暫存器分配或指令順序。
而是引入等價圖，也就是e-graph式的表示方法，再疊加規範化雜湊、對稱歸約和支配關係剪枝。
在同一組數學輸入輸出語義下，那些能夠被證明只差在暫存器命名、無依賴指令重排、冗餘中間量或區域性等價重寫上的候選序列，會被摺疊到同一個狀態節點裡。
生成器吐出的不再是一行行C程式碼或彙編。
而是一張巨大的狀態圖。
每一個節點，不再代表一段具體程式碼，而代表一組輸入輸出語義相同、並且己經被規範化的中間狀態。
每一條邊，才真正對應著一次實質性的，可落地的底層原語變換或機器指令變換。
搜尋空間，在廢土的第八年，第一次被從物理意義上狠狠壓了下來。
第十一年，為了進一步對抗時間的消耗，江臨在系統底層加入了證據快取機制。
。次一明證去解求3Z呼新重要都統系，構結的似相到遇尋搜次一每，去過
。存儲久永後化列序被會程過明證其，態狀價等的過證驗被有所，在現
。用複被樣一木積搭像以可明證的語原域區
。據證置前的分部組路網模規大更為作接首以可，明證確正的路網子層底
。變蛻生發始開lenreK-SPM
。機明證慧智的理定間中累積自會，憶記有擁臺一像始開，尋搜拙笨的尾到推頭從都次每個一像再不它
。層三分拆地晰清，斷斬刀揮統系明證的沌混而大龐將臨江，年三十第
。層語原象，層一第
。不水滴得義定被上義語學數的粹純在先首，心核微等k-pot、數位中、秩求、擇選、序排
？麼什是佈分料資的輸
？麼什是求要定穩序排的出輸
？值複重在存中列陣許允否是
？制機兵哨在存否是界邊法算演
。流分確明就層一這在須必，理值殊特的零號符帶及以字數非的中算運點浮、較比數整，是的要重最
。層示表間中與碼始原，層二第
。去過弄糊價等來起看它的飄飄輕句一用許允不對絕都，數函行cisnirtnI的寫編工手是還，RI MVLL、碼式程C是論無，層一這了到
。致一持保義語象層上與，集子義語的告宣被在RI保確，碎開拆地無輯邏學數被層一這在要都全，理的數lamroned對臺平同不及以，誌標常異、式模舍、序排零負正、播傳NaN的中較比點浮、則規斷截的時換轉數整度寬同不、義語繞迴模的數整號符無、為行義定未的位溢數整號符有、為行義定未的彰昭名惡中準標言語C
。層碼機，層三第
