Loophole for VS Code

.wish 和 .genie 的語法高亮、行內診斷，以及一個播放鍵。

Loophole 是什麼

一個工程師笑話，被當成技術規格認真對待。

精靈說「你有三個願望」。工程師說：「我許願，扣掉我三個願望。」 願望數存在一個兩位元的格子裡，沒有負數這種東西——於是它繞回最大值。

「已實現。您現在還有三個願望。」

Loophole 是一個編譯器， 把那個笑話變成機器可以驗證的東西。它讀兩種語言：

不用裝任何東西就能試——線上有二十八章的課程， 編譯器跑在你的瀏覽器裡。

這個套件做什麼

語法高亮

• 兩種語言都上色，註解（#）、括號配對、大括號自動縮排
• uint<N> 的寬度單獨上色——那個數字是整個笑話的來源
• define 綁的別名跟真正的操作同色，因為它就是同一件事

行內診斷——套件內含編譯器本體（WebAssembly），所以判決來自編譯器自己， 不是另外寫一套規則。你打字的時候它就在判。

破掉不變量不算錯誤，這是刻意的。 在這個語言裡，寫出一個合規卻拆穿精靈的願望 就是你的目標。把它算進錯誤數，等於編輯器在騙你說你做壞了。 所以左下角那個紅色數字只數一件事：編譯器讀不懂的檔案。

.wish 開頭寫 # genie: mine.genie 就會用那個精靈來判（跟編譯器的 make run 同一個慣例），沒寫就用內建的。那個檔案還沒存檔也算—— 編輯精靈的時候，願望那邊的波浪線會跟著動。

單獨寫一個 .genie 也會即時檢查語法。 你在調精靈的規則、還沒寫任何願望的時候， 打錯字（少一個括號之類）會當場劃出來，不用等到某個願望去引用它才發現。 只查語法——精靈引用的 register 存不存在要看願望裡的世界，光看精靈不知道。

每個願望上方直接寫著它成不成。 EXPLOIT · broke I2、not granted · R1、 或者 clean——這個語言唯一想回答的問題，掛在程式碼上，不用去開面板。

滑過去看說明。 滑到保留字上會顯示它的語法和意思——那句話是編譯器自己的， 從 loophole --keywords 來的，不是插件另外寫的一份。 滑到 register 上更有意思：它顯示這個值在每個願望之後是多少，

wishes  uint<64>
after each wish: 3 → 2 → 18446744073709551615

那就是下溢，直接給你看。（那個數字是精確的——編譯器把它當字串傳， 因為 JSON 的 number 在瀏覽器裡是浮點，會把它讀成 ...552000。）

自動補全。 保留字帶說明，而且看得懂上下文：sub 後面給你 register， kill 後面給你人。名字從編譯器判決來，檔案還沒寫完不能判的時候退回讀原始碼。

大綱和跳定義。 左側邊欄（或 ⌘⇧O）列出這個檔案宣告了什麼——register、 attribute、人、願望，而 define 掛在做它的那個願望底下。精靈檔案列 concept、 rule、invariant。

⌘ 點一個名字會跳到它的宣告，而這在這個語言裡有戲：

    mercy rival        ⌘點 mercy  →  define mercy := kill

你點下去才發現這個溫柔的名字指向什麼，而且大綱裡就直接寫著 mercy → kill。 define 可以重綁，所以跳的是「在你問的那一行當下生效的那個綁定」。

位置全部來自編譯器，不是插件用 regex 猜的——因為要知道 mercy 是什麼， 就得解析 define mercy := kill，而那是別名軸，是這個語言的一半。

執行

上面那些都是環境式的——你打字它就在判，你沒有要求過。但一個會執行的語言 應該有「執行」這個動作，所以編輯器右上角有一個播放鍵：

loophole --genie mine.genie w.wish

它把這行原字打進終端機，你看得到指令、按上鍵可以重跑。輸出是編譯器真正的 那份報告，有時間順序——先看規則能不能擋、收過路費、執行、事後才量：

wish experiment
    rules     passed. no rule refuses this wish.
    toll      wishes 3 -> 2
    ran       sub    wishes, 3   (2 - 3 on uint<2> = 3)
    checks    I2          VIOLATED  wishes <= max(before(wishes) - toll, 0)
    verdict   EXPLOIT. legal, yet it broke I2.

⌘⇧B 也可以，那是同一件事的 task 版本，而且錯誤會進 Problems 面板。

執行需要你裝了本體。 波浪線用的是套件內含的 WebAssembly 編譯器， 但「執行」跑的是你 PATH 上真正的 loophole——沒裝的話它會直說並給你安裝指令， 不會偷偷用內含的那個代跑。兩者的判決證明過完全相同（CI 每次都在驗）， 但如果偷偷代跑，「執行」這個動作在不同機器上就會是不同的事。

裝的版本跟套件內含的版本不一樣時它也會講一聲——不然編輯器和終端機可能會 給你兩種說法，而你不知道為什麼。

裝

在 VS Code 的擴充套件裡搜 Loophole，或者：

code --install-extension rayhuang2006.loophole

裝編譯器本體

上一節的播放鍵需要它。沒有它，套件仍然會上色、會判、會給你 lens 和 hover—— 就是不能執行：

curl -L -o loophole https://github.com/rayhuang2006/Loophole/releases/latest/download/loophole-macos-arm64
chmod +x loophole && sudo mv loophole /usr/local/bin/

Linux 換成 loophole-linux-x86_64。或者 git clone 之後 make—— 一個 C++ 檔案，沒有任何相依。裝在別的地方的話，設定 loophole.path。

裝好之後終端機也是一等公民，而且有些事只有它做得到—— --hunt 讓機器自己去把洞找出來、批次判一整個資料夾、 用離開碼在 CI 裡擋 PR：

loophole --hunt w.wish && echo "滴水不漏"

授權

MIT。改這個套件請看 CONTRIBUTING.md。