PO → SMT-LIB Conversion and Z3 Verification

Convert proof obligations (POs) generated by VDMJ into SMT-LIB format and verify them with Z3.

VDMJが生成した証明責務（PO）をSMT-LIB形式に変換し、Z3で自動検証する。

Prerequisites

Z3 Installation Check

which z3 || pip install z3-solver --break-system-packages

If Z3 is not available, guide the user through installation.

Z3がない場合はユーザーにインストールを案内する。

VDMJ Setup

Locate the VDMJ JAR using the same method as the verify-spec skill.

verify-specスキルと同じ方法でVDMJ JARを特定する。

Verification Flow

Step 1: PO Generation

Generate POs using the verify-spec procedure. Skip if PO output already exists.

verify-specの手順でPOを生成する。すでにPO出力がある場合はスキップ。

java -jar <VDMJ_JAR> -vdmsl <files...> -p 2>&1

Step 2: Convert Each PO to SMT-LIB

For each generated PO, perform the following conversion steps.

各POについて以下の手順で変換する。

2a. Generate Type Declarations

Scan all types appearing in the PO and declare them in SMT-LIB. Follow conversion rules in references/type-mapping-rules.md.

Key mappings:

• nat → Int + (>= x 0) constraint
• nat1 → Int + (>= x 1) constraint
• Record types → declare-datatypes + constructors/selectors
• seq1 of char → String + (> (str.len s) 0) constraint
• map K to V → uninterpreted sort + map_apply/map_dom functions
• set of T → (Array T Bool) characteristic function representation

POに出現する全型をSMT-LIBで宣言する。変換ルールは references/type-mapping-rules.md に従う。

2b. Generate Auxiliary Definitions

Define invariants, pre-conditions, and post-conditions referenced by the PO using define-fun:

POが参照する不変条件・事前条件・事後条件を define-fun で定義する:

(define-fun inv_TypeName ((x TypeSort)) Bool ...)
(define-fun pre_funcName ((arg1 Sort1) ...) Bool ...)

Include type constraints (nat/nat1 bounds, seq1 non-empty constraints) in invariant definitions.

2c. Convert the PO Body

Convert PO expressions following references/expression-mapping-rules.md.

PO式を references/expression-mapping-rules.md に従って変換する。

Key patterns:

• forall x:T & → (forall ((x T_smt)) (=> type_constraint ...)) — type constraint as antecedent
• exists x:T & → (exists ((x T_smt)) (and type_constraint ...)) — type constraint conjuncted
• mk_R(f1,f2):R pattern → single variable + let-bind fields
• let x = e in body → (let ((x e_smt)) body_smt)
• is_(e, bool) → usually true (trivial for total functions)

2d. Negate and check-sat

SMT-LIB verification uses refutation: "if the negation is unsatisfiable (unsat), the original proposition is valid":

SMT-LIBの検証は反駁法：「否定が充足不能（unsat）なら元の命題はvalid」:

(assert (not <PO_smt>))
(check-sat)

Step 3: Run Z3 Verification

Save the converted SMT-LIB file and verify with Z3:

変換したSMT-LIBファイルを保存し、Z3で検証する:

# Save to file
cat > /tmp/po_N.smt2 << 'SMTEOF'
<SMT-LIB content>
SMTEOF

# Verify with Z3
z3 /tmp/po_N.smt2

Step 4: Interpret and Report Results

Interpret Z3 output and report to the user in a clear manner.

Z3の出力を解釈し、ユーザーにわかりやすく報告する。

Z3 Output	Meaning	User Explanation (EN)	ユーザー向け説明 (JA)
unsat	Negation unsatisfiable → PO is valid	Proved: This property is logically derived from the spec	証明成功: この性質は仕様から論理的に導かれます
sat	Negation satisfiable → counterexample exists	Counterexample found: A case violating this property exists	反例発見: この性質を満たさないケースがあります
unknown	Z3 cannot decide	Undecidable: Z3 cannot automatically decide. Consider simplifying the spec	判定不能: Z3では自動判定できません。仕様の簡略化を検討してください
timeout	Time limit exceeded	Timeout: Verification did not complete in time	タイムアウト: 検証が時間内に完了しません

For sat results, have Z3 output the model (counterexample):

(check-sat)
(get-model)

Explain the counterexample in natural language. Example:

Counterexample: When name = "", email = "test@example.com", age = 200, the invariant age <= 150 is violated. 反例: name = "", email = "test@example.com", age = 200 のとき、不変条件 age <= 150 に違反します。

Step 5: Verification Summary

Summarize all PO results:

全PO結果をまとめて報告する:

## SMT Verification Summary / SMT検証サマリー

| # | Definition | PO Type | Z3 Result | Verdict |
|---|------------|---------|-----------|---------|
| 1 | User | invariant satisfiability | unsat | Proved / 証明成功 |
| 2 | findUser | map apply | unsat | Proved / 証明成功 |
| 3 | RegisterUser | state invariant | sat | Counterexample / 反例あり |

Proved: X/N
Counterexample found: Y/N
Undecidable: Z/N

Conversion Priority Order

Process POs in priority order rather than all at once:

すべてのPOを一度に変換するのではなく、優先度順に処理する:

1. invariant satisfiability — Simple structure, mechanical conversion / 構造が単純、変換が機械的
2. state init — Concrete value equality, usually trivial / 具体値の等値性、ほぼ自明
3. total function — is_(e, bool) pattern is usually trivial / 通常自明
4. subtype — Record invariant checking / レコード不変条件のチェック
5. map apply — Basics of map theory / 写像理論の基礎
6. func/op postcondition — Most complex, nested let expressions / 最も複雑、let式のネスト
7. state invariant — Requires state transition tracking / 状態遷移の追跡が必要
8. map compatible — Map operation compatibility / 写像操作の互換性

Handling Unconvertible Cases

Abandon conversion and report for these cases:

以下のケースでは変換を断念し、報告する:

• Higher-order functions: SMT-LIB is first-order logic; passing functions as values is unsupported
• Recursive function termination: Outside SMT solver scope
• Infinite set/sequence cardinality: card requires approximation even for finite sets
• Pattern match exhaustiveness: VDMJ's checker is more appropriate than SMT for cases expressions

高階関数、再帰関数の停止性、無限集合の基数、パターンマッチの網羅性は変換不可。

When conversion is impossible:

1. Provide a natural language explanation of the PO (from verify-spec)
2. Present hints for manual verification
3. Propose specification simplifications

Detailed References

• references/type-mapping-rules.md — Complete type conversion rules
• references/expression-mapping-rules.md — Complete expression conversion rules
• references/conversion-examples.md — Real PO conversion examples (verified with Z3)