Tezosスマートコントラクトのフォーマル検証

分析の目的がプロパティを証明し、スマートコントラクトのユーザーがそれらを理解するのを助けることであることに同意する場合、私はこう言います:

1. 値:ストレージの各要素が将来どのような値を取ることができるかを調査します.
2. 効果:将来どのような影響が発生する可能性があるかを調査します.通常、どのような転送がどのような条件で発生する可能性がありますか.
3. 所有権:ストレージのどの部分で変更をトリガーできるのか.

If we agree that the purpose of analyses is to both prove properties and help users of smart contracts to understand them, I would say:

1. Values: studying what values each element of the storage can take in the future.
2. Effects: studying what effects can occur in the future: typically what transfers can occur and on what conditions.
3. Ownership: who can trigger a change on what part of the storage.

これは大きな質問であり、私よりも資格のある人はたくさんいると思いますが、最初のガイダンスを提供します.

Coqに関する本であるSoftwareFoundationsで、彼らはImpと呼ばれる暗黙の言語について話します. Impの構文は次のとおりです.

 Z ::= X;;
Y ::= 1;;
WHILE ~(Z = 0) DO
    Y ::= Y * Z;;
    Z ::= Z - 1
END
 

これは、割り当てといくつかの単純なループとしてある程度簡単に理解できるはずです. ::=は代入用で、zが0になるまでwhileループを実行します.Pythonでは次のようになります.

 def foo(x):
    z = x
    y = 1
    while z != 0:
        y = y * z
        z -= 1
 

次に、シンボルの基礎となるロジックのいくつかを定義できます.たとえば、

 Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
  | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
  | AMult a1 a2 ⇒ (aeval a1) * (aeval a2)
  end.
 

これは算術演算を定義します.

次のように予約語を解析することもできます:

 Inductive com : Type :=
  | CSkip
  | CBreak (* <--- NEW *)
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).
 

次に、次のように、プログラムをCoqで定義されたこれらの型にマップできます.

 CSeq (CAss Z X)
        (CSeq (CAss Y (S O))
              (CWhile (BNot (BEq Z O))
                      (CSeq (CAss Y (AMult Y Z))
                            (CAss Z (AMinus Z (S O))))))
 

次に、形式論理を使用して、この言語で作成された関数またはステートメントについていくつかの証明を行うことができます.これは、zが4でない場合、xが2ではないことを証明する例です.

 Example ceval_example1:
  empty_st =[
     X ::= 2;;
     TEST X ≤ 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI
  ]⇒ (Z !-> 4 ; X !-> 2).
Proof.
  (* We must supply the intermediate state *)
  apply E_Seq with (X !-> 2).
  - (* assignment command *)
    apply E_Ass. reflexivity.
  - (* if command *)
    apply E_IfFalse.
    reflexivity.
    apply E_Ass. reflexivity.
Qed.
 

これまでに、スマートコントラクトへの適用がある程度明らかになることを願っています.スマートコントラクトをCoqに抽象化できれば、Coqを使用して、スマートコントラクトのいくつかのコンポーネントを厳密に証明できます. Coqのスマートコントラクトの条件を概説し、それをMichelsonにコンパイルする可能性もありますが、それは単なる可能性であり、その構築の証拠は見ていません.

ref: https://softwarefoundations.cis.upenn.edu/lf- current/Imp.html

So this is a huge question and I think there are many people more qualified than me, but I'll offer some initial guidance.

In Software Foundations, a book on Coq, they talk about an implied language called Imp. Imp has a syntax like:

Z ::= X;;
Y ::= 1;;
WHILE ~(Z = 0) DO
    Y ::= Y * Z;;
    Z ::= Z - 1
END

Which should be somewhat easily understood as assignment and some simple looping. ::= is for assignment, a while loop until z is 0. In python this would be:

def foo(x):
    z = x
    y = 1
    while z != 0:
        y = y * z
        z -= 1

We can then define some of the underlying logic for the symbols. For example,

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
  | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
  | AMult a1 a2 ⇒ (aeval a1) * (aeval a2)
  end.

This will define arithmetic operations.

You could also parse out reserved words, like:

Inductive com : Type :=
  | CSkip
  | CBreak (* <--- NEW *)
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

Then you could map the program to these defined types in Coq, like:

CSeq (CAss Z X)
        (CSeq (CAss Y (S O))
              (CWhile (BNot (BEq Z O))
                      (CSeq (CAss Y (AMult Y Z))
                            (CAss Z (AMinus Z (S O))))))

We can then make some proofs about the functions or statements made in this language using formal logic. Here is an example proving that if z is not 4, then x is not 2:

Example ceval_example1:
  empty_st =[
     X ::= 2;;
     TEST X ≤ 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI
  ]⇒ (Z !-> 4 ; X !-> 2).
Proof.
  (* We must supply the intermediate state *)
  apply E_Seq with (X !-> 2).
  - (* assignment command *)
    apply E_Ass. reflexivity.
  - (* if command *)
    apply E_IfFalse.
    reflexivity.
    apply E_Ass. reflexivity.
Qed.

By now I hope the application to a smart contract is somewhat apparent. If you could abstract the smart contract into Coq, you could use Coq to prove some components of your smart contract rigorously. There is also potential to outline conditions of a smart contract in Coq and compile it to Michelson, but that's just a possibility and I haven't seen any evidence of its construction.

ref: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html