証明が通った。で、その仕様は正しいの？ golang.tokyo #44 Warashi

証明が通った。 で、その仕様は正しいの？ Goの形式検証ツール Gobra に decimal を検証させてみた golang.tokyo #44 / Warashi 1

白状します AI に実装を書かせた AI に証明も書かせた 通ってしまった 2

自己紹介 太宰 晋之介 / GitHub: @Warashi Finatext で証券ビジネスプラットフォーム BaaS の開発 テストケースの重複や網羅性を気にしなくてよくなりたい 3

通ったからには、正しいのだろうか そう思いたい。 ただ、そう言い切るには、Gobra が何を保証してくれる道具なのかを 知っていなければならない 4

Gobra とは ETH Zurich 製、Go のための自動コード検証ツール Go のコードに事前条件と事後条件を書くと、あらゆる入力について成り立つか を証明してくれる // @ requires b != 0 // @ ensures res == a / b func Div(a, b int) (res int) { return a / b } Gobra found 0 errors. golang.tokyo #43 「Goのコードを数学的に証明する」（@sollniss）で詳しく紹介されています 5

題材：金額のための固定小数点 decimal float では 0.1 すら表せない // Decimal は coef * 10^-exp を表す固定小数点数 type Decimal struct { coef int exp int } 10進の桁をそのまま持つので、誤差なく足し引きできる 6

実装の int と、表したい値 実装が扱うのは、有界な int の寄せ集め 意味として表したいのは、桁あふれしない数 この乖離をどう仕様に書く？ 7

integer 型（Gobra に最近入った） ゴースト専用の数学的整数。上限も下限もない // ghost.gobra : Go のビルドからは見えないファイル ghost decreases n requires n >= 0 pure func pow10(n integer) (res integer) { return n == 0 ? 1 : 10 * pow10(n-1) } .go には置けない。仕様の世界にだけ存在する 8

実装を仕様に結びつける int で書いた実装が、 integer の理想と一致することを証明する // @ requires n >= 0 // @ ensures res == pow10(n) ← integer の世界と接続 func Pow10(n int) (res int) { res = 1 // @ invariant 0 <= i && i <= n // @ invariant res == pow10(i) for i := 0; i < n; i++ { res = res * 10 } return res } 9

桁を揃えたときの値 // ghost.gobra ghost requires d.exp >= 0 && s >= d.exp pure func scaled(d Decimal, s integer) integer { return d.coef * pow10(s-integer(d.exp)) } 指数 s に揃えたときの係数。これも integer なので、 何桁ずらしても溢れない 10

本題：桁を揃えた加算
// @ requires a.exp >= 0 && b.exp >= 0
// @ ensures res.exp >= a.exp && res.exp >= b.exp
// @ ensures scaled(res, res.exp) == scaled(a, res.exp) + scaled(b, res.exp)
func Add(a, b Decimal) (res Decimal) {
e := a.exp
if b.exp > e {
e = b.exp
}
ac := a.coef * Pow10(e-a.exp)
bc := b.coef * Pow10(e-b.exp)
return Decimal{coef: ac + bc, exp: e}
}
Gobra found 0 errors.
11

もう一つの Add // @ ensures res.coef == a.coef+b.coef // @ ensures res.exp == a.exp func AddBuggy(a, b Decimal) (res Decimal) { return Decimal{coef: a.coef + b.coef, exp: a.exp} } もっともらしく見えませんか？ 12

こちらも 0 errors Gobra found 0 errors. 0.1 + 0.02 = 0.3 桁を揃えていない。でも証明は通る 13

ところで、さっきの Add は $ gobra -p . Gobra found 0 errors. $ gobra -p . --overflow intro.go:6 a / b might cause integer overflow. decimal.go:10 res * 10 might cause integer overflow. decimal.go:29 a.coef * Pow10(e-a.exp) might cause integer overflow. buggy.go:7 {coef: a.coef + b.coef, ...} might cause integer overflow. Gobra found 4 errors. オーバーフロー検査は既定で無効。 Pow10(19) で溢れる 14

Gobra が保証していたもの 保証されたのは「実装が書いた仕様を満たす」ことだけだった その仕様が欲しい性質を表しているかは、誰も確かめていない どの設定で検証したかも、証明の中身の一部だった AI は実装も仕様も書ける。だが「何を保証したいか」は決められない 仕様を書くことが、検証の本体 15

AI に書かせた、あの証明 いま手元にある decimal の証明は、通っている 書かれた仕様を、私はまだ読み切っていない これから読む。そこからが検証だと思っている 16

まとめ Gobra：Go に事前条件と事後条件を書いて証明できる integer：桁あふれしない数を仕様に書けるゴースト型 証明が通る ≠ 正しい：仕様のレビューは人間の仕事 Gobra 本体（公式 Docker イメージ ghcr.io/viperproject/gobra） https://github.com/viperproject/gobra golang.tokyo #43「Goのコードを数学的に証明する」 https://sollniss.github.io/presentations/20260218_golang.tokyo.43/ 「自動推論シリーズスタート：Gobraでできること」 https://zenn.dev/finatext/articles/c4501622b2820b 「Gobra による複数粒度ロック証明への挑戦」 https://zenn.dev/finatext/articles/493a7e50-fb1e-4daf-a6de-5fbedb002842 17

• https://github.com/viperproject/gobra
• https://sollniss.github.io/presentations/20260218_golang.tokyo.43/
• https://zenn.dev/finatext/articles/c4501622b2820b
• https://zenn.dev/finatext/articles/493a7e50-fb1e-4daf-a6de-5fbedb002842