# 形式化驗證入門
==[第 1 集錄影](https://www.youtube.com/watch?v=CvIsM5-d8Nw)==
## 課程目標
* 針對形式化驗證的學習，導讀相關符號和背景知識
* 探討 $Hoare \space Logic$, $SAT/SMT$, $Model \space Checking$皆會用到最基本的邏輯 (Propositional Logic)
* 每段都有工具示範和習題
## Propositional Logic
==$\land$== ($\color{blue}{conjunction}$) 意思是「且」
==$\lor$== ($\color{blue}{disjunction}$) 意思是「或」
==$P \vdash Q$== 的意思就是「從 $P$ 證 $Q$」
==$P \vDash Q$== 代表「$P$ 為 True 的情況下 , $Q$ 成立」的意思
在上述兩組符號中，我們將
* $P$ 稱為 $\color{blue}{premises}$ (假定，假設；前提)
* $Q$ 稱為 $\color{blue}{conclusion}$ (結論；推論)
每個 $logic \space formula$ 都有語義，也就是真 ($True$) 與假 ($False$)
## $\land$ 與 $\lor$ 的消去規則與推導規則
:::success
$\land$
:::
- [ ] 消去規則 (elimination proof rule)
> $${A\land B\over A}\land e_1$$
>
> $${A\land B\over B}\land e_2$$
- [ ] 推導規則 (introduction proof rule)
> $${A\quad B\over A\land B}\land i$$
:::success
$\lor$
:::
- [ ] 消去規則 (elimination proof rule)
> $${{A \lor B } \quad \boxed{ A\\.\\.\\.\\C} \boxed{ B \\.\\.\\.\\ C } \over\ C}\lor e$$
- [ ] 推導規則 (introduction proof rule)
> $${ A \over {A \lor B} }\lor i_1$$
>
> $${ B \over {A \lor B} }\lor i_2$$
## 手寫 $A \land (B \lor C) \vdash(A \land B) \lor (A \land C)$ 證明
:::info
手寫示範
:::
## $\land$ 與 $\lor$ 的真值表
:::success
$\land$
:::
| | | |
| - | - | - |
| $P$ | $Q$ | $P \land Q$ |
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | F |
:::success
$\lor$
:::
| | | |
| - | - | - |
| $P$ | $Q$ | $P \lor Q$ |
| T | T | T |
| T | F | T |
| F | T | T |
| F | F | F |
:::success
$\Rightarrow$
:::
==$\Rightarrow$== 是推導 ($\color{blue}{Implication}$)
| | | |
| - | - | - |
| $P$ | $Q$ | $P \Rightarrow Q$ |
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
## $A \land (B \lor C) \vdash(A \land B) \lor (A \land C)$ 的真值表
==$A \land (B \lor C) \vdash(A \land B) \lor (A \land C)$== 可看成 ==$A \land (B \lor C) \Rightarrow(A \land B) \lor (A \land C)$==
| | | | | | | | | |
| - | - | - | - | - | - | - | - | - |
| $A$ | $B$ | $C$ | $B \lor C$ | $\color{blue}{A \land (B \lor C)}$ | $A \land B$ | $A \land C$ | $\color{red}{(A \land B) \lor (A \land C)}$ | $\color{blue}{A \land (B \lor C)} \color{green}{\Rightarrow} \color{red}{(A \land B) \lor (A \land C)}$ |
|T|T|T|T|$\color{blue}{T}$|T|T|$\color{red}{T}$|$\color{green}{T}$|
|T|T|F|T|$\color{blue}{T}$|T|F|$\color{red}{T}$|$\color{green}{T}$|
|T|F|T|T|$\color{blue}{T}$|F|T|$\color{red}{T}$|$\color{green}{T}$|
|T|F|F|F|$\color{blue}{F}$|F|F|$\color{red}{F}$|$\color{green}{T}$|
|F|T|T|T|$\color{blue}{F}$|F|F|$\color{red}{F}$|$\color{green}{T}$|
|F|T|F|T|$\color{blue}{F}$|F|F|$\color{red}{F}$|$\color{green}{T}$|
|F|F|T|T|$\color{blue}{F}$|F|F|$\color{red}{F}$|$\color{green}{T}$|
|F|F|F|F|$\color{blue}{F}$|F|F|$\color{red}{F}$|$\color{green}{T}$|
所以 $A \land (B \lor C) \vDash(A \land B) \lor (A \land C)$
## Soundness 與 Completeness
- [ ] Soundness (健全性)
在一個公理化系統中，如果一個 ==$P \vdash Q$== 是有效的 (證明存在)，就有 ==$P \vDash Q$==，這樣的特性稱為$Soundness$
- [ ] Completeness (完備性)
Completeness 則是反過來，在一個公理化系統下，如果有 ==$P \vDash Q$==，那麼 ==$P \vdash Q$== 就有個證明
## 小總結
對 $Propositional \space Logic$ 來說，是既 $Soundness$ 也 $Completeness$
在這兩個性質的形式化公理系統中，驗證一個 $logic \space formula$ , 可從算真假值，也可從寫證明下手，兩種方法有相同的效果
## Isabelle/HOL 示範 $A \land (B \lor C) \vdash(A \land B) \lor (A \land C)$ 證明
### Isabelle/HOL 介紹
[Isabelle/HOL](https://isabelle.in.tum.de/) 提供以下:
- [ ] $\lambda$ 演算 ($Typed \space \lambda 演算$)
[Week 1, Mon: intro](http://cs4161.web.cse.unsw.edu.au/week01A.pdf) 第 20 頁
> If I prove it on the computer, it is correct, right?
> No, because:
1. hardware could be faulty
2. operating system could be faulty
3. implementation runtime system could be faulty
4. compiler could be faulty
5. implementation could be faulty
6. logic could be inconsistent
7. theorem could mean something else
需要 Type 是因為第 6 個理由:
> logic could be inconsistent
Type 可減少 logic 產生自相矛盾的情況
- [ ] 檢查在某個公理化系統下的證明
能檢查證明，自然就可定義公理化系統
* 延伸閱讀: [一些公理化系統例子](https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/index.html)
以下案例說明 $\lambda$ 演算和 type 的影響
$\lambda$ 演算:
```Isabelle/HOL
term "(λy. x y) t"
```
type:
```Isabelle/HOL
lemma "1+2=3"
apply arith
```
### Isabelle/HOL 內 $\land$ 與 $\lor$ 的 proof rule
- [ ] ==$\land$== rule
> $conjI : [|\space A \space ;\space B\space |] \Rightarrow A \land B \\ conjE : [|\space A \land B \space ; [| \space A \space ; \space B \space |] \Rightarrow C \space |] \Rightarrow C$
- [ ] ==$\lor$== rule
> $disjI1 : A \Rightarrow A \lor B \\
disjI2 : A \Rightarrow B \lor A \\ disjE : [| \space A \lor B \space ; \space A \Rightarrow C \space ; \space B \Rightarrow C \space |] \Rightarrow C$
### 證明腳本
```Isabelle/HOL
theory Example imports Main
begin
lemma "A∧(B∨C)⟹(A∧B)∨(A∧C)"
apply(erule conjE)
apply (erule disjE)
apply (rule disjI1)
apply (rule conjI)
apply assumption
apply assumption
apply (rule disjI2)
apply (rule conjI)
apply assumption
apply assumption
done
end
```
## 練習題
$P \land Q\vdash Q \land P$
* [參考解答](https://gist.github.com/KevinKu/1d616da32f974a16bce53be8e5653ec1)
## 參考資訊
* [Introduction to Computational Logic](http://www.iis.sinica.edu.tw/~bywang/courses/comp-logic/)(每年會改)
* [一階邏輯](https://zh.wikipedia.org/wiki/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91)
* [$\lambda$演算](https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97)
* [新南威爾斯大學進階軟體驗證筆記](https://hackmd.io/AwEw7ArApgZgRjAtAQzGJAWAjFgbIgDlzjkWAGZcpoCBOKLAJnKA)
* [形式化驗證(Formal Verification)](https://hackmd.io/s/H1xxp3pF0)
* [Formal methods 共筆區](https://hackmd.io/MwMwpiBMBGDGkFoCcATALChaCM2AcCeArJNggAyqwDs01k15aaQA#formal-methods-共筆區)
* [FLOLAC 2017](http://flolac.iis.sinica.edu.tw/flolac17/doku.php)
* [Logic - FLOLAC '17](https://hackmd.io/s/SkEbrF-tZ)
---
## SAT/SMT
## Conjunctive Normal Form (CNF)
> $(A \lor B)\land (c = 2)\land (g > 8)$
像以上的 $\color{blue}{logic \space formula}$ 中間每個 form 都用 $\land$ 連接起來，稱為 Conjunctive Normal Form (CNF)
## $T_E$ 理論
$\Sigma_E:\{=,a,b,c,...,p,q,r\}$
* `=` 是等號的意思
* $a,b,c,...,p,q,r$ 是 logic formula
* $T_E$ 的 $E$ 代表 $Equality$
* $\Sigma_E$ 指的是符號集合
### $T_E$ 理論公理
* Reflexivity (反身性): $\color{blue}{\forall x. \space x=x}$
* Symmetry (對稱性): $\color{blue}{\forall x, y. \space x=y \Rightarrow y=x}$
* Transitivity (遞移性): $\color{blue}{\forall x, y, z. \space x=y,y=z \Rightarrow x=z}$
* Function congruence (功能一致性):
$\color{blue}{\forall x_1,\forall x_2,...,\forall x_n. \space \underset{i=1}{\overset{n}\land}(x_i=y_i) \Rightarrow f(x_1,...,x_n)=f(y_1,...,y_n)}$
### 等價關係 ($\color{blue}{Equivalence \space Relation}$)
* Reflexivity (反身性): $\color{blue}{\forall x. \space x=x}$
* Symmetry (對稱性): $\color{blue}{\forall x, y. \space x=y \Rightarrow y=x}$
* Transitivity (遞移性): $\color{blue}{\forall x, y, z. \space x=y,y=z \Rightarrow x=z}$
$T_E$ 理論公理前 3 條，就是所謂的等價關係。注意到 $\color{blue}{=}$ 是一種等價關係
#### 等價類 ($\color{blue}{Equivalence \space Class}$)
一個集合，給定一個等價關係，可把這集合分割成數個子集合，而子集合內的任兩個元素都滿足給定的等價關係，這樣的子集合稱為等價類
舉個例子:
集合 $\{a,b,c,d,e\}$
假如 $a=b,b=c,d=e$
那可以分割成兩個等價類:
$\{a,b,c\},\{d,e\}$
可看到 $a=b=c,d=e$
### $T_E$ 可滿足性的演算法
可滿足的意思：在某個前提，logic formula 是成立的 ($P \vDash Q$)
可滿足性就是討論 $P \vDash Q$ 或 $P \nvDash Q$ 的問題
這邊所講的演算法，會利用上面的等價類
舉例說明:
> $f^3(a)=a \land f^5(a)=a \land f(a)\neq a$
:::info
手寫示範
:::
## z3 驗證 C 程式
### z3 介紹
[z3下載](https://github.com/Z3Prover/z3)
在 z3 的 build 目錄下，輸入以下命令:
```shell
./z3 -in
```
隨後可進入命令交談模式。
### z3 使用案例
```z3
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert(and (and (= a b) (= b c)) (= a c)))
(check-sat)
```
輸出 $\color{blue}{sat}$，代表滿足
```z3
(declare-const a Int)
(assert(and (> a 10) (< a 5)))
(check-sat)
```
輸出 $\color{red}{unsat}$，代表不滿足
#### 驗證 C 程式
```clike
int show(int x) {
if (x < 10)
x = x - 1;
assert(x != 9);
return 0;
}
```
驗證 `show` 函式時，帶入任意的 int 數值，執行不會出現 assert 錯誤訊息
#### C code to SSA form
:::info
SSA 是 [Static Single Assignment](https://en.wikipedia.org/wiki/Static_single_assignment_form)
SSA 最主要的用途，是藉由簡化變數的特性，提升編譯器最佳化的能力。舉例來說：
```
y := 1
y := 2
x := y
```
不難見到，第一行變數的數值指派並非必要，因為 y 在第二行再次指派，y 的數值在第三行被使用，一個程式通常會進行定義可達性分析 (reaching definition analysis) 來測定。在 SSA 下，將會變成以下形式：
> y~1~ := 1
> y~2~ := 2
> x~1~ := y~2~
其中 y~1~ 表示第 1 次變數 y 的數值指派，y~2~ 表示第 2 次，後者又用於變數 x 的第 1 次指派。顯然 y~1~ 沒被用到，所以編譯器可輕易消除。
再者考慮以下形式:
由於涉及分支指令，w~2~ 的數值指派究竟是圖片左邊的 y~1~，還是右邊的 y~2~ 呢？編譯器不能貿然確認，這時就引入 $\phi$ 函數，根據程式運作的路徑來選擇 y~1~ 或 y~2~
:::
首先把 C 程式轉成 SSA 形式:
```clike
int show(int x0) {
if (x0 < 10)
x1 = x0 - 1;
x2 = phi(x0, x1)
assert(x2 != 9);
return 0;
}
```
phi 為 $\phi$ 函數
#### SSA form to SMT Formula
> $(x0 < 10 ∧ x1 = x0 - 1 ∧ x2 = x1 ∧ x2 = 9) ∨
(x0 ≥ 10 ∧ x2 = x0 ∧ x2 = 9)$
assert 內是 $\color{red}{x2!=9}$
這不是 $T_E$ 可接受的 $logic \space formula$
所以轉為算 $\color{blue}{x2=9}$
然後是兩個 CNF 用 ==$\lor$== 連接
由 =$\lor$== 的真值表，要算兩次的 SMT
先算 $(x0 < 10 ∧ x1 = x0 - 1 ∧ x2 = x1 ∧ x2 = 9)$
再算 $(x0 ≥ 10 ∧ x2 = x0 ∧ x2 = 9)$
只要其中一個是滿足，整個 $logic \space formula$ 就滿足了
整個 $logic \space formula$ 滿足 , 那就代表執行會有錯誤訊息
來看寫成的z3 code是如何
- [ ] $(x0 < 10 ∧ x1 = x0 - 1 ∧ x2 = x1 ∧ x2 = 9)$
```z3
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (and (< x0 10) (= x1 (- x0 1))) (and (= x2 x1) (= x2 9) ) ))
(check-sat)
```
- [ ] $(x0 ≥ 10 ∧ x2 = x0 ∧ x2 = 9)$
```z3
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (or (= x0 10) (> x0 10)) (and (= x2 x0) (= x2 9) ) ))
(check-sat)
```
結果:
```shell
$ ./z3 -in
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (and (< x0 10) (= x1 (- x0 1))) (and (= x2 x1) (= x2 9) ) ))
(check-sat)
unsat
```
不滿足
```shell
$ ./z3 -in
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (or (= x0 10) (> x0 10)) (and (= x2 x0) (= x2 9) ) ))
(check-sat)
unsat
```
也是不滿足
因此兩者在執行不會出現 assert 錯誤訊息
對照 C 程式編譯後的執行結果:
```clike
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
int show(int x) {
if (x < 10)
x = x - 1;
assert(x != 9);
return 0;
}
int main() {
show(3);
return 0;
}
```
結果:
```shell
$ gcc -o test test.c
$ ./test
$
```
果然沒出現 assert 錯誤訊息，我們可見到形式化驗證的威力：在不需要執行程式的狀況下，充分檢驗各種輸入造成的影響。
在 [軟體缺失導致的危害](https://hackmd.io/s/B1eo44C1-) 提到 1970 年代推出的首款廣體民航客機波音 747 軟體由大約 40 萬行程式碼構成，而 2011 年引進的波音 787 的軟體規模則是波音 747 的 16 倍，約 650 萬行程式碼。換言之，你我的性命緊繫於一系列極為複雜的軟體系統之中，如果程式開發者總是撰寫程式碼後，只用上述有限的數值輸入並對結果，勢必無法顧及全面，難保日後不出問題，這也是為何形式化驗證大量用於航空和醫療這類關鍵的領域中。
## 練習題
```clike=
int show(int x) {
if (x <= 10)
x = x - 1;
assert(x != 9);
return 0;
}
```
當輸入某個整數值時，執行會出現 assert 錯誤訊息
* [參考解答](https://gist.github.com/KevinKu/58416f46dc4ba3421591065471722740)
## 參考資料
* [SMT](http://flolac.iis.sinica.edu.tw/flolac17/doku.php?id=course:smt)
* [你所不知道的 C 語言: 編譯器原理和最佳化](https://hackmd.io/s/Hy72937Me)
* [z3使用文件](https://rise4fun.com/z3/tutorial)
* [Z3求解器指南（一）](http://blog.csdn.net/alu_xd/article/details/52169885)
* [Z3求解器指南（二）](http://blog.csdn.net/alu_xd/article/details/52174022)
* [Software Foundations](https://softwarefoundations.cis.upenn.edu/)
###### tags: `formal verification`
Sign in with Wallet
Connect another wallet