なぜ私のプログラムは拒否されたのか
Keleusma の検証器は、WCET および WCMU 解析が有界であることを証明できないプログラムを拒否します。これは意図的なものです。この言語の価値提案は実行時間とメモリに関する確定的な境界であり、境界を引く最も安全な場所は解析の現在の能力です。完全な記述については LANGUAGE_DESIGN.md を参照してください。
この文書は、検証器のエラーメッセージを根本原因に対応付け、書き換えを提案します。エラーメッセージは src/verify.rs と src/compiler.rs が生成する実際の文字列です。検証器がプログラムを拒否した場合は、エラーメッセージの部分文字列でこの文書を検索してください。
拒否の分類
拒否されたプログラムは、拒否が根本的なものか解析上のものかによって区別される 2 つのカテゴリに分類されます。
第 1 のカテゴリ、証明可能に境界がないもの。 その構文は、構造上、実行時に境界のない実行を許します。境界が存在しないため、外部の証明書がない限り、将来の検証器の改善によっても許容されることはありません。対処法は、プログラムを境界付けされた形式に書き換えることです。
第 2 のカテゴリ、境界付けされているがまだ証明されていないもの。 実行時の振る舞いは事実として境界付けされていますが、静的な証明がまだ実装されていません。将来の解析は、表層言語を変えることなく、そのようなプログラムを許容される集合へ移せます。対処法は、現在の解析が扱える形式にプログラムを書き換えるか、将来の検証器の拡張を待つことです。
これらのカテゴリが一貫しているのは、この言語が拒否を安全性の性質として扱うためです。Vm::new によって受理されるプログラムは、その境界が証明されたものであって、原理的に境界が存在するものではありません。設計上の根拠については LANGUAGE_DESIGN.md を参照してください。
一般的な拒否メッセージ
MakeRecursiveClosure
type error: closures are not supported; V0.2.0 admits only direct calls and
trait dispatch under the conservative-verification stance. Rewrite as a
top-level fn or trait method.
カテゴリ. 第1。V0.2.0 Phase 4はクロージャ系全体を引退させました — クロージャのオペコードはOpの列挙型から消え、Value::Funcランタイムヴァリアントは消え、型検査器がExpr::Closureを直接却下します。診断は読み込み時の検証器ではなく型検査器から表面化します — 却下がパイプラインで早めに動いたので、エラーメッセージは下げられたオペコードではなく構文に名前を付けます。
トリガー. let束縛が自分自身を名前で参照し、自分の環境スロットを取り込むクロージャ値を生成する。
let factorial = |n: Word| if n <= 1 { 1 } else { n * factorial(n - 1) };
書き換え. Keleusmaのローカルは不変です。ループ間の累積は、データセグメント(これ自体はloop-分類のエントリーポイントからのみアクセス可能)か、フォールドを実行するホスト供給のネイティブのどちらかを必要とします。2つの構造的な書き換えが適用できます。
最初はエントリーポイントをloopに再分類し、データブロックを通じて反復間で累積することです。
data state { result: Word }
loop main(input: Word) -> Word {
state.result = state.result * input;
let _next = yield state.result;
state.result
}
ホストはスクリプトを駆動する前に、vm.set_data(slot, value)を通じてstate.resultを意味のある開始値に初期化しなければなりません。
2つ目はホスト側のフォールドネイティブを登録してfnから呼ぶことです。
use math::fold_product
fn main() -> Word {
math::fold_product([1, 2, 3, 4, 5])
}
選択は、反復回数が無界か(ホストがloopを駆動する)、有限でコンパイル時に既知か(ホストがフォールドネイティブを登録する)によります。
第一級関数参照
first-class function references are not supported in V0.2.0; rewrite `name` as
a direct call site or as a trait-bounded generic
カテゴリ. 第1。V0.2.0 Phase 4は、それが奉仕したクロージャと並んでOp::PushFuncとOp::CallIndirectオペコードを引退させました。トップレベル関数名への裸の参照が(呼び出し位置ではなく)値位置にあったときは、以前はOp::PushFuncにコンパイルされました。コンパイラは今、上記の診断でそのパターンを却下します。
トリガー. let束縛が関数値を保持する、または関数値が引数を流れる。
fn increment(x: Word) -> Word { x + 1 }
fn main() -> Word {
let f = increment; // 却下: 第一級関数参照
f(5)
}
書き換え. 間接ディスパッチを直接呼び出しまたはトレイトメソッドで置き換えます。
fn increment(x: Word) -> Word { x + 1 }
fn main() -> Word {
increment(5)
}
以前は第一級関数を使用していた合成パターンについて、V0.2.0 はモノモーフィゼーションを通じて impl が静的にディスパッチされるトレイト境界付きジェネリックを受理します。トレイトのサーフェスについては LANGUAGE_DESIGN.md を参照してください。
ループ反復境界を抽出できない（Loop Iteration Bound Not Extractable）
loop at instruction <ip> has no statically extractable iteration bound; strict
mode requires loops with fall-through bodies to match the canonical for-range
pattern
カテゴリ. 第2。実行時のループ回数は実行時に既知の値で境界づけられるかもしれませんが、現在の検証器はNがコンパイル時定数の正準的なfor i in 0..N形式からだけ反復回数を抽出します。
トリガー. forループが、終端がパラメータまたは関数呼び出しの結果である範囲を反復する。
fn process(n: Word) -> Word {
for i in 0..n { ... }
0
}
書き換え. コンパイル時定数の境界を使うか、長さが既知の配列を反復します。
fn process() -> Word {
for i in 0..10 { ... }
0
}
境界が真に実行時既知の場合、プログラムは今日の安全な検証サーフェスの外にあり、ループ境界推論の拡張を待つか、ホストが無界のリスクを受け入れた上でVm::new_uncheckedを通じて出荷するかのどちらかです。
再帰呼び出しを検出（Recursive Call Detected）
recursive call detected during WCMU topological sort
カテゴリ. 第1。fnまたはyield関数での直接または相互再帰は言語設計によって却下されます。loopだけが循環的実行を許容し、それも生産的なRESETサイクルを通じてのみです。
トリガー. fnが直接または別のfnを経由して自分自身を呼ぶ。
fn count_down(n: Word) -> Word {
if n <= 0 { 0 } else { count_down(n - 1) }
}
書き換え. 再帰的クロージャの場合と同様に、書き換えは反復回数が有界かどうかによります。コンパイル時に有界な回数の場合は、forループを使って、結果が累積ではなく反復回数によって決まるように計算を構造化します。無界の回数の場合は、循環的な振る舞いをトップレベルのloopブロックに移します。そこでは生産性ルールがそれを許容します。
カウントダウンの純粋関数型書き換えは、スクリプトがステップごとの出力を必要としない場合は無操作です。
fn count_down(n: Word) -> Word {
for _ in 0..n { let _step = 1; }
0
}
ステップごとの出力が必要な場合は、上の再帰的クロージャの書き換えで示したように、loopスクリプトのデータセグメントを通じて累積します。
ストリームブロックに yield がない（Stream Block Missing Yield）
Stream block must contain at least one Yield
カテゴリ. 第1。loop関数は生産性保証を満たすために、反復ごとにyieldしなければなりません。本体にyieldを含まないループ関数は、無界の静かな計算を許容してしまいます。
トリガー. yieldを呼ばない本体を持つloop宣言。
loop main(input: Word) -> Word {
input * 2
}
書き換え. ループ本体にyield式を追加します。
loop main(input: Word) -> Word {
let doubled = input * 2;
let _next = yield doubled;
doubled
}
再入可能ブロックに yield がない（Reentrant Block Missing Yield）
Reentrant block must contain at least one Yield
カテゴリ. 第1。yield-分類された関数は、すべての経路にyield式を含むか、分類が間違っているかのどちらかです。
トリガー. yieldとして宣言されたが本体が決してyieldしない関数。
書き換え. 本体にyield式を追加するか、関数が実際には直接返るのなら分類をfnに変えます。
リソース境界を超過（Resource Bounds Exceeded）
verify_resource_bounds: arena capacity <cap> bytes is below WCMU bound
of <wcmu> bytes
カテゴリ. 精神的には第2、効果的には第1。プログラムはメモリで有界ですが、構成されたアリーナが境界に対して小さすぎます。
トリガー. アリーナが手動で構成されて小さすぎるか、スクリプトのWCMUが期待を超えている。
書き換え. auto_arena_capacity_forを使ってアリーナをモジュールから大きさを決めるか、明示的な容量を増やします。
let cap = keleusma::vm::auto_arena_capacity_for(&module, &[])?;
let arena = Arena::with_capacity(cap);
let vm = Vm::new(module, &arena)?;
WCMU自体が驚きの場合は、verify::module_wcmu出力をチャンクごとに調べて高コストの経路を特定します。検査パターンの例はexamples/wcmu_basic.rsを参照してください。
ブロック境界エラー（Block Boundary Errors）
EndIf at <ip> with no matching If
EndLoop at <ip> with no matching Loop
Break at <ip> outside any Loop block
カテゴリ. 第1。バイトコードレベルのブロック境界が一貫していません。これらのメッセージはユーザーのプログラム問題というよりも、ソースからバイトコードへのパイプラインのバグを示しています。Keleusmaユーザーがこれらのどれかに遭遇した場合、問題はコンパイラのバグです。プロジェクトに対してissueを提出してください。
サーフェスはコンパイルされるが検証器が却下するとき
保守的検証スタンスは、サーフェス言語が検証器の許容集合より広いことを受け入れます。字句解析、構文解析、型検査、コンパイルに成功したプログラムが、それでもVm::newで却下されることがあります。これは第2カテゴリが動いている姿です — 言語は構文を記述するので、検証器はそれを近似ではなく正確に却下できます。
標準的な応答はプログラムを書き換えることです。代替の応答は次のとおりです。
Vm::new_uncheckedを使って無界リスクを明示的に受け入れる。これはWCET契約の外の意図的な誤用で、そのように文書化されています。- 将来の検証器の改善を待ちます。BACKLOG.md が保留中の検証器拡張を追跡しています。B3 のクロージャと B14 の CallIndirect フロー解析は V0.1 時代のエントリであり、V0.2.0 のフェーズ 4 がクロージャサーフェスを完全に削除することで置き換えました。
- 解析が許容すべきと考える却下されたプログラムでissueを提出する。作業例は解析の改善を優先付けするのに価値があります。
相互参照
- LANGUAGE_DESIGN.md が保守的検証の立場の正典的な記述です。
- EXECUTION_MODEL.md が構造検証器の動作を説明しています。
- BACKLOG.md が将来の検証器拡張を追跡しています。
src/verify.rsは実際の却下ロジックとエラーメッセージ文字列を含みます。