verify コマンドを追加 #52

cedretaber · 2024-10-26T12:01:57Z

概要

https://hackmd.io/xQoyRGzyRHGPFEK9XU70Ew

lean/z3 を使って validation を行う verify コマンドを追加。

src/ast2theorem.ml は dangtv/BIRDS から持ってきました。
中身を整えるのは別の PR でやりたいです。

動作確認

lean/z3 の環境が必要です。
lean は 3.4.2 、 z3 は 4.8.7 のバージョンで動作確認をしています。

以下の Docker Image を利用すると簡単に環境を作ることができます。
https://github.com/proof-ninja/docker-verify-BIRDS

成功

source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
% view definition:
tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2.
% putdelta
+tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q), Q > 2.
% constraints
_|_ :- tracks3(T,R,A,Q), Q <= 2.

$ dune exec verify examples/verify_valid1.dl

...

>>> verified by lean: correct
The program satisfies all delta disjointness, getput and putget

失敗

source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
% view definition:
tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2.
% putdelta
+tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q).
% constraints
_|_ :- tracks3(T,R,A,Q), Q <= 2.

$ dune exec verify examples/verify_invalid_getput1.dl

...

>>> verified by lean: correct
Fatal error: exception Birds.Utils.ChkErr("\n\nInvalidity: Property getput is not validated \nExit code: 1\nError messange: /tmp/b8bad8.lean:7:4: error: z3 was unable to prove the goal\nstate:\ntracks2 : string \226\134\146 \226\132\164 \226\134\146 string \226\134\146 \226\132\164 \226\134\146 Prop\n\226\138\162 (\226\136\128 (x : string) (x_1 : \226\132\164) (x_2 : string) (x_3 : \226\132\164),\n       (\194\172tracks2 x x_1 x_2 x_3 \226\136\168 tracks2 x x_1 x_2 x_3 \226\136\167 x_3 > 2) \226\136\168 \194\172tracks2 x x_1 x_2 x_3) \226\136\167\n    \226\136\128 (x : string) (x_1 : \226\132\164) (x_2 : string) (x_3 : \226\132\164),\n      ((\194\172tracks2 x x_1 x_2 x_3 \226\136\168 \194\172x_3 > 2) \226\136\168 tracks2 x x_1 x_2 x_3) \226\136\168 tracks2 x x_1 x_2 x_3\nHint: use option --counterexample to generate a counterexample")

bin/verify.ml

cedretaber · 2024-10-26T12:03:15Z

src/verify.ml

+  else
+    (* if (!cex_generation) then (print_endline !counterexample_mess; exit 0)
+    else *)
+      raise (Utils.ChkErr !verification_mess)


例外投げるのではなく、普通に出力して終了しても良いかもしれない。

元のコードからなのかもしれないけれど
>>> verified by lean: correct
は変わらないのだろうか 🤔
correctではなさそう

確かに correct ではないですね 😇

コマンドライン引数の hint とか、現状と明らかに合ってない出力とかも今はそのままにしているので、動作確認してもらって良さそうなら直します 🙏

cedretaber · 2024-10-26T12:05:52Z

verify.ml のコードは古い main.ml から切り取ってきて少し手直ししたものだけど、書き方を全体的に修正しても良いかもしれない。

ref を使わずに結果とエラー表示とを取得するようにする
深くネストした if をどうにかする
エラー内容を文字列で作るのではなく型で表現するなどして、表示用の出力は別のロジックとする
適宜コードを関数に分割する

動作確認をして良さそうなら上のような修正を入れても良いと思う。

cedretaber · 2024-11-06T11:23:20Z

実際に処理されている Lean コードの例

`examples/verify_valid1.dl` から生成されたもの。

import bx

local attribute [instance] classical.prop_decidable

theorem disjoint_deltas {tracks2: (string → (int → (string → (int → Prop))))} {tracks3: (string → (int → (string → (int → Prop))))}: (((∃A, (∃Q, (∃R, (∃T, ((tracks3 T R A Q) ∧ (¬ (Q > (2: int)))))))) → false) → ((∃COL0, (∃COL1, (∃COL2, (∃COL3, (((tracks3 COL0 COL1 COL2 COL3) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3))) ∧ (((tracks2 COL0 COL1 COL2 COL3) ∧ (¬ (tracks3 COL0 COL1 COL2 COL3))) ∧ (COL3 > (2: int)))))))) → false)):=
    begin
    z3_smt
    end

import bx

local attribute [instance] classical.prop_decidable

theorem getput {tracks2: (string → (int → (string → (int → Prop))))}: (true → (((∃COL0, (∃COL1, (∃COL2, (∃COL3, ((((tracks2 COL0 COL1 COL2 COL3) ∧ (¬ ((tracks2 COL0 COL1 COL2 COL3) ∧ (COL3 > (2: int))))) ∧ (COL3 > (2: int))) ∧ (tracks2 COL0 COL1 COL2 COL3)))))) ∨ (∃COL0, (∃COL1, (∃COL2, (∃COL3, ((((tracks2 COL0 COL1 COL2 COL3) ∧ (COL3 > (2: int))) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3))) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3)))))))) → false)):=
    begin
    z3_smt
    end

import bx

local attribute [instance] classical.prop_decidable

theorem putget {tracks2: (string → (int → (string → (int → Prop))))} {tracks3: (string → (int → (string → (int → Prop))))}: (((∃A, (∃Q, (∃R, (∃T, ((tracks3 T R A Q) ∧ (¬ (Q > (2: int)))))))) → false) → (∀ALBUM, (∀QUANTITY, (∀RATING, (∀TRACK, (((((tracks2 TRACK RATING ALBUM QUANTITY) ∧ (¬ (((tracks2 TRACK RATING ALBUM QUANTITY) ∧ (¬ (tracks3 TRACK RATING ALBUM QUANTITY))) ∧ (QUANTITY > (2: int))))) ∨ ((tracks3 TRACK RATING ALBUM QUANTITY) ∧ (¬ (tracks2 TRACK RATING ALBUM QUANTITY)))) ∧ (QUANTITY > (2: int))) ↔ (tracks3 TRACK RATING ALBUM QUANTITY))))))):=
    begin
    z3_smt
    end

`examples/verify_invalid_getput1.dl` から生成されているもの。

import bx

local attribute [instance] classical.prop_decidable

theorem disjoint_deltas {tracks2: (string → (int → (string → (int → Prop))))} {tracks3: (string → (int → (string → (int → Prop))))}: (((∃A, (∃Q, (∃R, (∃T, ((tracks3 T R A Q) ∧ (¬ (Q > (2: int)))))))) → false) → ((∃COL0, (∃COL1, (∃COL2, (∃COL3, (((tracks3 COL0 COL1 COL2 COL3) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3))) ∧ ((tracks2 COL0 COL1 COL2 COL3) ∧ (¬ (tracks3 COL0 COL1 COL2 COL3)))))))) → false)):=
    begin
    z3_smt
    end

import bx

local attribute [instance] classical.prop_decidable

theorem getput {tracks2: (string → (int → (string → (int → Prop))))}: (true → (((∃COL0, (∃COL1, (∃COL2, (∃COL3, (((tracks2 COL0 COL1 COL2 COL3) ∧ (¬ ((tracks2 COL0 COL1 COL2 COL3) ∧ (COL3 > (2: int))))) ∧ (tracks2 COL0 COL1 COL2 COL3)))))) ∨ (∃COL0, (∃COL1, (∃COL2, (∃COL3, ((((tracks2 COL0 COL1 COL2 COL3) ∧ (COL3 > (2: int))) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3))) ∧ (¬ (tracks2 COL0 COL1 COL2 COL3)))))))) → false)):=
    begin
    z3_smt
    end

import bx

local attribute [instance] classical.prop_decidable

theorem putget {tracks2: (string → (int → (string → (int → Prop))))} {tracks3: (string → (int → (string → (int → Prop))))}: (((∃A, (∃Q, (∃R, (∃T, ((tracks3 T R A Q) ∧ (¬ (Q > (2: int)))))))) → false) → (∀ALBUM, (∀QUANTITY, (∀RATING, (∀TRACK, (((((tracks2 TRACK RATING ALBUM QUANTITY) ∧ (¬ ((tracks2 TRACK RATING ALBUM QUANTITY) ∧ (¬ (tracks3 TRACK RATING ALBUM QUANTITY))))) ∨ ((tracks3 TRACK RATING ALBUM QUANTITY) ∧ (¬ (tracks2 TRACK RATING ALBUM QUANTITY)))) ∧ (QUANTITY > (2: int))) ↔ (tracks3 TRACK RATING ALBUM QUANTITY))))))):=
    begin
    z3_smt
    end

hiroshi-cl · 2024-11-13T11:38:26Z

src/ast2theorem.ml

+
+(*
+(* take a view update datalog program and generate the theorem of checking whether all delta relations are disjoint *)
+let lean_theorem_of_disjoint_delta (debug:bool) prog =


ここコメントアウトされているのはなぜだろうか？

ast2theoremはファイル丸ごとコピーしてるからここをいじるのは別プルリクかも

そうですね、このファイルはそのまま持ってきただけです。
コマンドの動作確認が取れたら直していくのが良いかなと考えています。

PR の概要にその旨記載しました。

hiroshi-cl · 2024-11-13T11:38:52Z

src/ast2theorem.ml

+
+(*
+(* (unnecessary now see sourcestability_sentence_of_stt in ast2fol.ml) take a view update datalog program and generate SourceStability constraint (put s v = s) for its view update strategy *)
+let sourcestability_of_stt (debug:bool) prog =


ここもコメントアウトか

hiroshi-cl · 2024-11-13T11:42:42Z

動作確認をして良さそうなら上のような修正を入れても良いと思う。

次のプルリクで良さそう

yoshihiro503 · 2024-11-18T14:08:05Z

@cedretaber
timeoutが指定できたいとのことです。
--timeout みたいなオプションでtimeoutの値が指定できるようにできますでしょうか？

cedretaber · 2024-11-19T23:02:44Z

--timeout オプションを追加しました。

`--timeout` オプションの使い方

--timeout に続けて timeout の秒数を渡してください。

$ dune exec verify -- examples/verify_test1.dl --timeout 30

従来通りオプション無しでも利用できます。この場合、 timeout はデフォルトの180秒になります。

注意点

上記の通り、 dune exec verify の後に -- を入れてからファイル名、 timeout などの引数を渡してください。
この -- を忘れると、 dune コマンドに対するオプションと見做されエラーとなります。

cedretaber · 2024-11-19T23:05:02Z

📝
オプションを取るコマンドが増えてきたので、コマンドラインオプション用のライブラリを導入して整理した方が良いかも。

hiroyukikato · 2025-01-09T10:52:21Z

Thanks! LGTM

cedretaber self-assigned this Oct 26, 2024

cedretaber commented Oct 26, 2024

View reviewed changes

bin/verify.ml Outdated Show resolved Hide resolved

cedretaber commented Oct 26, 2024

View reviewed changes

hiroshi-cl reviewed Nov 13, 2024

View reviewed changes

cedretaber added 5 commits January 15, 2025 20:11

Add verify command.

fe95eee

Remove inexplicable messages and commented-out codes.

2784ad4

Add --timeout option.

a143336

Fix parse_argv function.

bb9f532

Use Arg module to parse args.

c8e97c0

cedretaber force-pushed the add-verify-command branch from d2a7a76 to c8e97c0 Compare January 15, 2025 11:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

verify コマンドを追加 #52

verify コマンドを追加 #52

cedretaber commented Oct 26, 2024 •

edited

Loading

cedretaber Oct 26, 2024

hiroshi-cl Oct 27, 2024

cedretaber Oct 30, 2024

cedretaber commented Oct 26, 2024

cedretaber commented Nov 6, 2024

hiroshi-cl Nov 13, 2024

hiroshi-cl Nov 13, 2024

cedretaber Nov 13, 2024

cedretaber Nov 13, 2024

hiroshi-cl Nov 13, 2024

hiroshi-cl commented Nov 13, 2024

yoshihiro503 commented Nov 18, 2024

cedretaber commented Nov 19, 2024

cedretaber commented Nov 19, 2024

hiroyukikato commented Jan 9, 2025

verify コマンドを追加 #52

Are you sure you want to change the base?

verify コマンドを追加 #52

Conversation

cedretaber commented Oct 26, 2024 • edited Loading

概要

動作確認

成功

失敗

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cedretaber commented Oct 26, 2024

cedretaber commented Nov 6, 2024

実際に処理されている Lean コードの例

examples/verify_valid1.dl から生成されたもの。

examples/verify_invalid_getput1.dl から生成されているもの。

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hiroshi-cl commented Nov 13, 2024

yoshihiro503 commented Nov 18, 2024

cedretaber commented Nov 19, 2024

--timeout オプションの使い方

注意点

cedretaber commented Nov 19, 2024

hiroyukikato commented Jan 9, 2025

cedretaber commented Oct 26, 2024 •

edited

Loading

`examples/verify_valid1.dl` から生成されたもの。

`examples/verify_invalid_getput1.dl` から生成されているもの。

`--timeout` オプションの使い方