はじめに

こんにちは。弊社はVerify APIという、公的個人認証サービス（JPKI）によって作成された署名の検証を行うAPIを提供しています。

このVerify APIはConnect を用いて開発されており、RPCのインターフェース記述には Protocol Buffers という言語が使用されています。

Protocol Buffers と Common Expression Language

Protocol ButtersはRPCのリクエスト・レスポンスがどのような構造になっているのかを記述するために作成された言語です。さらに、protovalidate という機能を用いることで、データのバリデーションを行うことができます。

たとえば、ユーザのID（UUID）を受け取り、対象ユーザの名前を返却するUserというRPCがある場合、以下のようにProtocol Buffersのコードを書くことができます。

message UserRequest {
  string id = 1 [(buf.validate.field).string.uuid = true];
}

message UserResponse {
  string name = 1;
}

string id = 1 で引数のidが文字列型であることを宣言し、[(buf.validate.field).string.uuid = true] によって、uuid フォーマットであることを宣言しています。

さて、このprotovalidateですが、uuid = true のような組み込みのバリデーションのほかに、ユーザ定義のバリデーションも作成することができます。

例えば、以下のように書くことで「numは偶数でなければならない」というバリデーションを記述することができます。

この expression: に記述する文字列は、 Common Expression Language（CEL）と呼ばれる言語で記述されます。

message UserRequest {
  string id = 1 [(buf.validate.field).string.uuid = true];
  uint32 num = 2;
  
  option (buf.validate.message).cel = {
    id: "even"
    message: "num must be even"
    expression: "num % 2 == 0"
  };
}

このCELの言語仕様はGitHubで公開されており、誰でもアクセスすることができます。

CELの停止性

CELの言語仕様の冒頭を読むと、以下のように書いてあります。

• terminating: CEL programs cannot loop forever;

すなわち、CELの実行は必ず停止する、ということです。

今回のブログでは、CELの実行が必ず停止することを頑張って証明していきたいと思います。

CELの言語仕様を引用し、全て説明を行うと証明の量が非常に多くなってしまいますので、ある程度省略して説明をしていきます。

本来、CELには

論理演算子として && , ||
算術演算子として + , - , * , / , %
比較演算子として < , <= , == , !=

などさまざまな演算子や構文が存在しますが、今回は || * を取り上げ、残りの演算子や構文についての説明は省略します。

説明していない二項演算子については演算以外ほぼ同じ定義となるため、省略してもわかると思います。

証明に使用する概念

そもそも、証明の前に「プログラムの実行」や「プログラムの停止」について数学的に考えなければなりません。

例えば、簡単なCELの式として、1 + 2 + 3 + 4 を考えます。

直観的には、これを「実行」すると 10 という数になるでしょう（pythonのように、式を入力してエンターを押すとその結果が表示されるプログラムがあると考えてください）。

頭の中では、この 10 という結果を得るために

1 + 2 + 3 + 4 → (1 + 2) + 3 + 4 →3 + 3 + 4
3 + 3 + 4 → (3 + 3) + 4 → 6 + 4
6 + 4 → 10

のように「実行」したのではないでしょうか？（色々な計算順序があるのでこれは一例です）

(1 + 2) + 3 + 4 の(1 + 2) や、(3 + 3) + 4 の(3 + 3)を元の式の部分式と呼びます。

全体の式を部分式に分解し、それらを次々と「実行」していけば、最終的に全体の式を「実行」した結果を得られます。

このように、式が与えられた時にその結果を得ることを評価（Evaluation）と言い、「実行した結果」を値（Value）と言います。

では、評価ができる部分式はどのような式なのでしょうか？

上記の例は、1 + 2 + 3 + 4 を評価するためには、まず 1 + 2 + 3 を評価する必要があり、1 + 2 + 3 を評価するためには ……と言い換えることもきます。

最終的に、1 + 2 の評価を行い、3 + 3 の評価、6 + 4 の評価、と進んでいきます。

想像のついた方もいると思いますが、x + y は両辺が値の時に評価が可能となります。

このように、全体の式を評価したい場合、「引数がすべて値の部分式」から評価を行うことで、全体の式の評価が行えます。

（これは、プログラムの構文木を帰りがけ順で評価していくことに対応します）

評価を数学的に扱うために、評価を「一気に結果まで計算する」のではなく、１ステップずつ進む関係として定義します。

これを単一ステップ評価と呼び、記号で E → E' と書いて、「式 E は１ステップ評価すると式 E' になる」という意味にします。

例えば、

1 + 2 は１ステップで 3 になる
3 + 3 は１ステップで 6 になる

ので、

1 + 2 → 3
3 + 3 → 6

のように書けます。

また、E0 → E1 → … → En のように、０回以上のステップで E0 から En に到達する時、E0 →* En と書きます。

例えば、1 + 2 + 3 + 4 →* 10 となります。

単一ステップ評価の規則は、しばしば次のような推論規則の形で書かれます。

E1 → E1' E2 → E2' …… En → En'
──────────────────
E → E'

この記法は、

「E1 がE1'に評価され、かつ、E2がE2'に評価され、…、EnがEn'に評価されるなら、EがE'に評価される」

という意味を表しています。

単一ステップ評価では、上側に「部分式が１ステップ進む」といった条件を書き、下側に「全体の式が１ステップ進む」という事実を書くことで、評価規則を定義します。

+ の例であれば、以下のように書け、（左辺の）Xが式X'に評価されるならば、X + Y という式は X' + Y に評価される、と読みます。

$\displaystyle \frac{e_1 \to e_1'}{e_1 + e_2 \to e_1' + e_2}$

この記法を用いCELの評価規則を定義し、「CELの式Eに対し、必ず値Vが存在し、E →* Vとなる」という命題で「必ず停止する」ことを表現します。

以下は、CELの文法を参考に私が考えたCELの評価規則の一部です。

全てを記載すると量が非常に多くなるので、簡単なものだけ記載しています。

論理和 || の評価規則

左辺が値（真偽値）でない場合、左辺のステップを進める規則

$\displaystyle \frac{e_1 \to e_1'}{e_1 \mathbin{\|} e_2 \to e_1' \mathbin{\|} e_2}$

左辺が値（真偽値）の場合、式全体を論理和の結果にする規則

$\displaystyle \frac{}{\text{true} \mathbin{\|} e \to \text{true}}\qquad \frac{}{\text{false} \mathbin{\|} e \to e}$

掛け算 * の評価規則

左辺、または右辺の部分式が値（数値）でない場合、部分式のステップを進める規則

$\displaystyle \frac{e_1 \to e_1'}{e_1 \times e_2 \to e_1' \times e_2}\qquad \frac{e_2 \to e_2'}{e_1 \times e_2 \to e_1 \times e_2'}$

部分式が値（数値）の場合、式全体を計算結果にする規則

$\displaystyle \frac{}{n_1 \times n_2 \to n_3} \quad (n_3 = n_1 \times n_2 \text{かつ} n_1, n_2, n_3\text{は数値})$

停止性の証明の概略

前置きが長くなりましたが、停止性の証明の概略を説明します。

直感的には「部分式の評価が必ず終了するなら、元の式の評価も終了する」と言えそうです。

この記事では、

E → E1 → E2 → ... のように無限にステップが続く列は存在しないこと（整礎性）と、

任意の式 E について、ある値 V が存在して E →* V が成り立つ。

より正確に言うと、CEL の実行中に実行時エラーとなる可能性があるので、

任意の式 E について、値 V またはエラー err が存在して E →* V または E →* err が成り立つ。

ことの証明を目指します。

それぞれ、

１ステップ評価関係 E → E’ について、これが無限に続かないこと
値でない（かつ、エラーでもない）式ならば必ず１ステップ進めることができること

を証明すれば十分なので、この証明を目指します。

CELの場合、評価を１ステップ進めると、評価後の「式のサイズ」（＝構文木のサイズ）が必ず減少するように評価規則を定義することができます。

これにより、ステップを進めると、式のサイズが最小であるものになるまで評価が進むことが言え、それ以上は評価が進められないことが示せます。

同様に、評価規則を、値でない式ならば必ず１ステップ進めるように定義するので、後者は直ちに成り立つことが言えます。

評価規則

評価規則は、CELの言語仕様に記載されている文法と評価から定義を行います。

例えば掛け算 X * Y の場合、想定する挙動としては「評価するとXとYを掛け算した結果になる」となるはずです。

これを意識して、まず、部分式が値の場合の評価規則を考えます。

$\displaystyle \frac{}{n_1 \times n_2 \to n_3} \quad (n_3 = n_1 \times n_2 \text{かつ} n_1, n_2, n_3\text{は数値})$

この評価規則を使用するためには、部分式が値でなければいけないので、それぞれの部分式を値になるまで評価する規則を考えます。

$\displaystyle \frac{e_1 \to e_1'}{e_1 \times e_2 \to e_1' \times e_2}\qquad\frac{e_2 \to e_2'}{e_1 \times e_2 \to e_1 \times e_2'}$

すべての文法構造について、まず「値の場合にどんな結果になるか」の評価規則を定義し、それを使用するために部分式を値にしていく評価規則を定義する、という流れで評価規則を定義することができます。

評価規則を定義する時に気をつけるべき点として、CELの仕様に

Because CEL is free of side effects, the order of evaluation among sub-expressions is not guaranteed.

とあり、どの部分式を評価していくかは任意となっています。

厳密に評価規則を定義する場合、これを反映した評価規則とする必要があります。

例えば、掛け算 X * Y の場合

部分式Xを評価し、部分式Yを評価する
部分式Yを評価し、部分式Xを評価する

という、複数の順序が可能な評価規則にする必要があります。

ただし、CELは短絡評価を採用しているため、関係演算子 &&、|| の右辺は、左辺の評価が終了し値になってから、評価が必要な場合にのみ評価されます。

$\displaystyle \frac{e_1 \to e_1'}{e_1 \mathbin{\|} e_2 \to e_1' \mathbin{\|} e_2}$

$\displaystyle \frac{}{\text{true} \mathbin{\|} e \to \text{true}}\qquad\frac{}{\text{false} \mathbin{\|} e \to e}$

例えば、(1 == 1) || (1 / 0 == 1) という式の場合、以下のようなステップとなります。

短絡評価のため、右辺に 1 / 0 が含まれているにもかかわらず、これは評価されずに全体の評価結果とは true となります。

$\displaystyle \frac{1 = 1 \to \text{true}}{(1 = 1) \mathbin{\|} (1 \div 0 = 1) \to \text{true} \mathbin{\|} (1 \div 0 = 1)}\qquad \frac{}{\text{true} \mathbin{\|} (1 \div 0 = 1) \to \text{true}}$

このように、評価順序に気をつけながら全ての文法規則について評価規則を定義していきます。

CELの関数呼び出しについては、関数名に指定された（メタな）意味を元に、結果が返却されるものとして扱います。

また、実行時エラーについては、値ではないものの、「これ以上評価できないもの」として扱い、式のサイズも１として扱います。

例えば、a.b のようなフィールドアクセスの時に、aがmapでない場合や、フィールドが存在しない場合にエラーに評価されるように定義します。

停止性

このようにCELの文法に従って定義された評価規則は、評価後は必ず式のサイズが減少します。

本来は文法構造に関する帰納法によって厳密に証明しなければなりませんが、今回は概略のみ説明します。

例えば、掛け算の評価規則の、部分式の評価を進める場合

$\displaystyle \frac{e_1 \to e_1'}{e_1 \times e_2 \to e_1' \times e_2}\qquad\frac{e_2 \to e_2'}{e_1 \times e_2 \to e_1 \times e_2'}$

であれば、評価後の部分式のサイズは評価前より小さいことが言えます（帰納法の仮定から）。

これと、掛け算そのもの（X * Y）の式のサイズは、（Xの式のサイズ）＋（Yの式のサイズ）＋１であることから、評価前のサイズより評価後のサイズが小さいことが示せます。

また、部分式が全て値になり、「式そのもの」の評価が進む場合

$\displaystyle \frac{}{n_1 \times n_2 \to n_3} \quad (n_3 = n_1 \times n_2 \text{かつ} n_1, n_2, n_3\text{は数値})$

も、「式そのもの」から値というようにサイズは減少します。

このように、文法に従って素直に評価規則を定義するだけで、全ての演算子について評価後の式のサイズが減少することが示せます。

これにより、１ステップ評価関係をすすめると、必ずサイズが減少するため、いずれ「サイズが最も小さい式」に辿り着きます。

この「サイズが最も小さい式」は値（もしくは実行時エラー）なので「CELの評価は必ず停止する」ことが言えます。

おまけ：停止性の証明の挑戦

この証明を定理証明言語である Lean4 で証明しようとしたのですが、量が多いのと時間が足りずに証明までいかず、評価規則の定義までしか完成しませんでした…。

せっかく定義したのでいくつかのコア部分を記載しますが、途中までしか完成していないので見なくても大丈夫です（量が多いので折りたんでいます）。

文法定義部分

文法と見比べるとほぼそのままなのがわかると思います

-- Mapのキーの型
inductive CELPrimitiveValue : Type where
  | bool : Bool → CELPrimitiveValue
  | int : Int → CELPrimitiveValue
  | uint : Nat → CELPrimitiveValue
  | string : String → CELPrimitiveValue
  deriving BEq, Repr

-- CELの値型
inductive CELValue : Type where
  | primitive : CELPrimitiveValue → CELValue
  | double : Float → CELValue
  | bytes : String → CELValue  -- バイト列を文字列として表現
  | null : CELValue
  | list : List CELValue → CELValue
  | map : List (CELPrimitiveValue × CELValue) → CELValue  -- キーと値のペアのリストとして表現
  | message : MessageName → List (String × CELValue) → CELValue  -- Protocol Bufferメッセージ型（メッセージ名、フィールドのリスト）
  | celtype : CELType → CELValue  -- 型を表す値（type関数の結果）
  deriving BEq, Repr

mutual
  -- 最上位の式（三項演算子を含む）
  inductive Expr : Type where
    | conditional : ConditionalOr → ConditionalOr → Expr → Expr  -- condition ? true_expr : false_expr
    | fromConditionalOr : ConditionalOr → Expr
  deriving BEq

  -- 論理OR（||）
  inductive ConditionalOr : Type where
    | or : ConditionalOr → ConditionalAnd → ConditionalOr  -- left || right
    | fromConditionalAnd : ConditionalAnd → ConditionalOr
  deriving BEq

  -- 論理AND（&&）
  inductive ConditionalAnd : Type where
    | and : ConditionalAnd → Relation → ConditionalAnd  -- left && right
    | fromRelation : Relation → ConditionalAnd
  deriving BEq

  -- 関係演算
  inductive Relation : Type where
    | relation : Relation → RelOp → Addition → Relation  -- left op right
    | fromAddition : Addition → Relation
  deriving BEq

  -- 加算・減算（+ -）
  inductive Addition : Type where
    | add : Addition → Multiplication → Addition  -- left + right
    | sub : Addition → Multiplication → Addition  -- left - right
    | fromMultiplication : Multiplication → Addition
  deriving BEq

  -- 乗算・除算・剰余（* / %）
  inductive Multiplication : Type where
    | mul : Multiplication → Unary → Multiplication  -- left * right
    | div : Multiplication → Unary → Multiplication  -- left / right
    | mod : Multiplication → Unary → Multiplication  -- left % right
    | fromUnary : Unary → Multiplication
  deriving BEq

  -- 単項演算
  inductive Unary : Type where
    | not : Nat → Member → Unary  -- !...! member (連続する!の数)
    | neg : Nat → Member → Unary  -- -...- member (連続する-の数)
    | fromMember : Member → Unary
  deriving BEq

  -- メンバーアクセス
  inductive Member : Type where
    | member : Member → String → Member  -- member.field
    | receiverCall : Member → String → ExprList → Member  -- member.func(args...)
    | index : Member → Expr → Member  -- member[index]
    | fromPrimary : Primary → Member
  deriving BEq

  -- 基本式
  inductive Primary : Type where
    | literal : CELValue → Primary  -- LITERAL
    | var : String → Primary  -- IDENT (["."] IDENT)
    | varCall : String → ExprList → Primary  -- IDENT(args...) (["."] IDENT "(" [ExprList] ")")
    | paren : Expr → Primary  -- (Expr)
    | list : ExprList → Primary  -- [ExprList]
    | map : MapInits → Primary  -- {MapInits}
    | message : MessageName → FieldInits → Primary  -- ["."] SELECTOR { "." SELECTOR } "{" [FieldInits] [","] "}"
  deriving BEq

  inductive ExprList : Type where
    | cons : Expr → ExprList → ExprList
    | nil : ExprList
  deriving BEq

  inductive MapInits : Type where
    | cons : Expr → Expr → MapInits → MapInits
    | nil : MapInits
  deriving BEq

  inductive FieldInits : Type where
    | cons : String → Expr → FieldInits → FieldInits
    | nil : FieldInits
  deriving BEq
end

部分式が値の時の評価規則

文法構造で定義したfrom〇〇〜をCoersionとして使用しています。

inductive CELPrimStepResult : Type where
  | next : Expr → CELPrimStepResult
  | done : CELValue → CELPrimStepResult
  | error : CELError → CELPrimStepResult
  deriving BEq

def PrimStepRel (lhs: CELValue) (op: RelOp) (rhs: CELValue) : CELPrimStepResult := match lhs, op, rhs with
-- Bool
  | .primitive (v₁:Bool), RelOp.lt, .primitive (v₂:Bool) => (.done (decide (v₁ < v₂)))
  | .primitive (v₁:Bool), RelOp.le, .primitive (v₂:Bool) => (.done (decide (v₁ <= v₂)))
  | .primitive (v₁:Bool), RelOp.gt, .primitive (v₂:Bool) => (.done (decide (v₁ > v₂)))
  | .primitive (v₁:Bool), RelOp.ge, .primitive (v₂:Bool) => (.done (decide (v₁ >= v₂)))
  | .primitive (v₁:Bool), RelOp.eq, .primitive (v₂:Bool) =>  (.done (v₁ == v₂))
  | .primitive (v₁:Bool), RelOp.ne, .primitive (v₂:Bool) => (.done (v₁ != v₂))
-- Int
  | .primitive (v₁:Int), RelOp.lt, .primitive (v₂:Int) => (.done (decide (v₁ < v₂)))
  | .primitive (v₁:Int), RelOp.le, .primitive (v₂:Int) => (.done (decide (v₁ <= v₂)))
  | .primitive (v₁:Int), RelOp.gt, .primitive (v₂:Int) => (.done (decide (v₁ > v₂)))
  | .primitive (v₁:Int), RelOp.ge, .primitive (v₂:Int) => (.done (decide (v₁ >= v₂)))
  | .primitive (v₁:Int), RelOp.eq, .primitive (v₂:Int) => (.done (v₁ == v₂))
  | .primitive (v₁:Int), RelOp.ne, .primitive (v₂:Int) => (.done (v₁ != v₂))
-- Nat
  | .primitive (v₁:Nat), RelOp.lt, .primitive (v₂:Nat) => (.done (decide (v₁ < v₂)))
  | .primitive (v₁:Nat), RelOp.le, .primitive (v₂:Nat) => (.done (decide (v₁ <= v₂)))
  | .primitive (v₁:Nat), RelOp.gt, .primitive (v₂:Nat) => (.done (decide (v₁ > v₂)))
  | .primitive (v₁:Nat), RelOp.ge, .primitive (v₂:Nat) => (.done (decide (v₁ >= v₂)))
  | .primitive (v₁:Nat), RelOp.eq, .primitive (v₂:Nat) => (.done (v₁ == v₂))
  | .primitive (v₁:Nat), RelOp.ne, .primitive (v₂:Nat) => (.done (v₁ != v₂))
-- String
  | .primitive (v₁:String), RelOp.lt, .primitive (v₂:String) => (.done (decide (v₁ < v₂)))
  | .primitive (v₁:String), RelOp.le, .primitive (v₂:String) => (.done (decide (v₁ <= v₂)))
  | .primitive (v₁:String), RelOp.gt, .primitive (v₂:String) => (.done (decide (v₁ > v₂)))
  | .primitive (v₁:String), RelOp.ge, .primitive (v₂:String) => (.done (decide (v₁ >= v₂)))
  | .primitive (v₁:String), RelOp.eq, .primitive (v₂:String) => (.done (v₁ == v₂))
  | .primitive (v₁:String), RelOp.ne, .primitive (v₂:String) => (.done (v₁ != v₂))
-- Float
  | .double (v₁:Float), RelOp.lt, .double (v₂:Float) => (.done (decide (v₁ < v₂)))
  | .double (v₁:Float), RelOp.le, .double (v₂:Float) => (.done (decide (v₁ <= v₂)))
  | .double (v₁:Float), RelOp.gt, .double (v₂:Float) => (.done (decide (v₁ > v₂)))
  | .double (v₁:Float), RelOp.ge, .double (v₂:Float) => (.done (decide (v₁ >= v₂)))
  | .double (v₁:Float), RelOp.eq, .double (v₂:Float) => (.done (v₁ == v₂))
  | .double (v₁:Float), RelOp.ne, .double (v₂:Float) => (.done (v₁ != v₂))
-- bytes
  | .bytes (v₁:String), RelOp.lt, .bytes (v₂:String) => (.done (decide (v₁ < v₂)))
  | .bytes (v₁:String), RelOp.le, .bytes (v₂:String) => (.done (decide (v₁ <= v₂)))
  | .bytes (v₁:String), RelOp.gt, .bytes (v₂:String) => (.done (decide (v₁ > v₂)))
  | .bytes (v₁:String), RelOp.ge, .bytes (v₂:String) => (.done (decide (v₁ >= v₂)))
  | .bytes (v₁:String), RelOp.eq, .bytes (v₂:String) => (.done (v₁ == v₂))
  | .bytes (v₁:String), RelOp.ne, .bytes (v₂:String) => (.done (v₁ != v₂))
-- null
  | .null, RelOp.lt, .null => (.done false)
  | .null, RelOp.le, .null => (.done false)
  | .null, RelOp.gt, .null => (.done false)
  | .null, RelOp.ge, .null => (.done false)
  | .null, RelOp.eq, .null => (.done true)
  | .null, RelOp.ne, .null => (.done false)
-- list
  | .list (v₁:List CELValue), RelOp.eq, .list (v₂:List CELValue) => (.done (v₁ == v₂))
  | .list (v₁:List CELValue), RelOp.ne, .list (v₂:List CELValue) => (.done (v₁ != v₂))
-- map
  | .map (v₁:List (CELPrimitiveValue × CELValue)), RelOp.eq, .map (v₂:List (CELPrimitiveValue × CELValue)) => (.done (v₁ == v₂))
  | .map (v₁:List (CELPrimitiveValue × CELValue)), RelOp.ne, .map (v₂:List (CELPrimitiveValue × CELValue)) => (.done (v₁ != v₂))
-- message
  | .message (name₁:MessageName) (field₁: List (String × CELValue)), RelOp.eq, .message (name₂:MessageName) (field₂: List (String × CELValue)) => (.done (name₁ == name₂ && field₁ == field₂))
  | .message (name₁:MessageName) (field₁: List (String × CELValue)), RelOp.ne, .message (name₂:MessageName) (field₂: List (String × CELValue)) => (.done (name₁ != name₂ || field₁ != field₂))
-- celtype
  | .celtype (v₁:CELType), RelOp.eq, .celtype (v₂:CELType) => (.done (v₁ == v₂))
  | .celtype (v₁:CELType), RelOp.ne, .celtype (v₂:CELType) => (.done (v₁ != v₂))
-- in_
  | v₁, RelOp.in_, .list (v₂:List CELValue) => (.done (v₂.any (λ e => e == v₁)))
  | .primitive v₁, RelOp.in_, .map (v₂:List (CELPrimitiveValue × CELValue)) => (.done (v₂.any (λ e => e.1 == v₁)))
-- default
  | _, _, _ => (.error .type_mismatch)

inductive PrimStep {ρ: VarEnv} {M: MsgEnv} {Φ: FuncEnv} : Expr → CELPrimStepResult → Prop
-- conditional
  | conditionalTrue e₁ e₂ : PrimStep (Expr.conditional true e₁ e₂) (.next e₁)
  | conditionalFalse e₁ e₂ : PrimStep (Expr.conditional false e₁ e₂) (.next e₂)
-- or
  | orTrue e : PrimStep (ConditionalOr.or true e) (.done true)
  | orFalse e : PrimStep (ConditionalOr.or false e) (.next e)
-- and
  | andFalse e : PrimStep (ConditionalAnd.and false e) (.done false)
  | andTrue e : PrimStep (ConditionalAnd.and true e) (.next e)
-- rel
  | rel v₁ op v₂ (h₁: IsValueRelation v₁) (h₂: IsValueAddition v₂): PrimStep (Relation.relation v₁ op v₂) (PrimStepRel (relation_to_CELValue h₁) op (addition_to_CELValue h₂))
-- add, sub
  | addInt (v₁: Int) (v₂: Int) : PrimStep (Addition.add v₁ v₂) (.done (v₁ + v₂))
  | addFloat (v₁: Float) (v₂: Float) : PrimStep (Addition.add v₁ v₂) (.done (v₁ + v₂))
  | subInt (v₁: Int) (v₂: Int) : PrimStep (Addition.sub v₁ v₂) (.done (v₁ - v₂))
  | subFloat (v₁: Float) (v₂: Float) : PrimStep (Addition.sub v₁ v₂) (.done (v₁ - v₂))
-- mul, div, mod
  | mulInt (v₁: Int) (v₂: Int) : PrimStep (Multiplication.mul v₁ v₂) (.done (v₁ * v₂))
  | mulFloat (v₁: Float) (v₂: Float) : PrimStep (Multiplication.mul v₁ v₂) (.done (v₁ * v₂))
  | divInt (v₁: Int) (v₂: Int) : PrimStep (Multiplication.div v₁ v₂) (.done (v₁ / v₂))
  | divFloat (v₁: Float) (v₂: Float) : PrimStep (Multiplication.div v₁ v₂) (.done (v₁ / v₂))
  | modInt (v₁: Int) (v₂: Int) : PrimStep (Multiplication.mod v₁ v₂) (.done (v₁ % v₂))
-- not, neg
  | unaryNot n (v: Bool) : PrimStep (Unary.not n v) (.done (if n % 2 = 0 then v else !v))
  | unaryNegInt n (v: Int) : PrimStep (Unary.neg n v) (.done (if n % 2 = 0 then v else -v:Int))
  | unaryNegFloat n (v: Float) : PrimStep (Unary.neg n v) (.done (if n % 2 = 0 then v else -v:Float))
-- member, receiverCall, index
-- Member.memberのアクセスされる側がCELValueのmessageなら評価が進む
  | memberMessage name messageValue field :
    PrimStep
      (Member.member (CELValue.message name messageValue) field)
      (match (messageToFun name messageValue).2 field with
        | some v => .done v
        | none => (.error .no_such_field))
  | memberMap mapValue key:
    PrimStep (Member.member
      (CELValue.map mapValue) key)
      (match mapToFun mapValue key with
        | some v => .done v
        | none => (.error .no_such_field))
  | receiverCall receiver name values (valueMember: IsValueMember receiver) (valueExprList: IsValueExprList values):
    PrimStep
      (Member.receiverCall receiver name values)
      -- 関数の実装を呼び出す
      (let exprListWithReceiver := ExprList.cons receiver values;
      let exprListWithReceiverIsValue := IsValueExprList.cons receiver values valueMember valueExprList;
      let args := exprListToArgs exprListWithReceiverIsValue;
        match Φ name with
        | some func =>
          if h: func.arity = exprListWithReceiver.length
          then (func.impl (Eq.mp (congrArg (λ n => Fin n → CELValue) (Eq.symm h)) args))
          else (.error .no_matching_overload)
        | none => (.error .no_matching_overload))
-- indexはmapとlistのCELValueであれば進む
  | indexMap mapValue key:
    PrimStep
      (Member.index (CELValue.map mapValue) (CELValue.primitive key))
      (match mapToFun mapValue key with
        | some v => .done v
        | none => (.error .no_such_field))
  | indexListInt listValue index:
    PrimStep
      (Member.index (CELValue.list listValue) (CELValue.primitive (index:Int)))
      (match Int.toNat? index with
        | some index => if h: index < listValue.length then .done (listValue.get (Fin.mk index h)) else (.error .no_such_index)
        | none => (.error .no_such_index))
  | indexListNat listValue index:
    PrimStep
      (Member.index (CELValue.list listValue) (CELValue.primitive (index:Nat)))
      (if h: index < listValue.length then .done (listValue.get (Fin.mk index h)) else (.error .no_such_index))
-- var, varCall, paren, list, map, message
  | var s : PrimStep (Primary.var s) (match ρ s with
    | some v => .done v
    | none => (.error .no_such_variable))
  | varCall s args (valueExprList: IsValueExprList args):
    PrimStep
      (Primary.varCall s args)
      (match Φ s with
        | some func =>
          if h: func.arity = args.length
          then CELEvalResultToCELPrimStepResult (func.impl (Eq.mp (congrArg (λ n => Fin n → CELValue) (Eq.symm h)) (exprListToArgs valueExprList)))
          else (.error .no_matching_overload)
        | none => (.error .no_matching_overload))
  | paren e : PrimStep (Primary.paren e) (.next e)
  | list es (h: IsValueExprList es): PrimStep (Primary.list es) (.done (CELValue.list (exprListToListCELValue h)))
  | map es (h: IsValueMapInits es): PrimStep (Primary.map es) (match mapInitsToMapCELValue h with
    | some fields => .done (CELValue.map fields)
    | none => (.error .type_mismatch))
  | message name fields (h: IsValueFieldInits fields): PrimStep (Primary.message name fields) (match fieldInitsToMessageCELValue name h with
    | (name, fields) => .done (CELValue.message name fields))