判決

Cella 的檢查以判決結束，不是布林。

判決	意思	附帶
Accept	兩個 kernel 都驗過	依賴的假設：某個 postulate、某條改寫規則、由 elaborator 判斷的終止性、模型照實作做的選擇
Reject	有錯	在哪裡、違反哪一條規則
Unknown	還不知道	原因：有洞、步數預算用完、kernel 表達不了、依賴了未知的東西

Accept 是組合出來的，不是回傳的

Accept 只能由判決的組合造出來：檢查器的任何一部分都不能回傳 true 就算通過。預算以步數計、不以時間，所以判決可以重現。

Unknown 會傳染

依賴 Unknown 的定義不是 Accept。欠定的答案（例如電路少了一顆地）是有證據的 Unknown：說得出缺什麼。帶誤差界的數值結論是 Accept 加一條額定假設；給不出憑證的求解器只能以假設出現。

其他語言的程式

C、C++、Arduino、Python 的程式，判決還會說出程式怎麼結束：結束碼與輸出、碰到的未定義行為與標準的條文，或依賴的實作選擇（例如未指定的求值順序走了哪一邊），列在 assumes 裡。

這種判決的每個問題有 kind（具體的理由，例如 ubOverflow）與 category（六種之一，宿主照它決定怎麼顯示）：

category	意思
error	程式錯了：檢查沒過，或碰到未定義行為
unsupported	模型還沒有這個構造（程式可能是對的）
indeterminate	算不出確定的結果：步數用完、行為未指定、程式在等輸入
termination	程式照定義結束：abort、未接住的例外
incomplete	程式有空的槽
invalid	程式的 JSON 不是一支程式

assumes 一律在（判決不依賴任何選擇時是空的），每一項寫出實作與選擇，宿主執行程式前可以拿來核對自己。