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.

所以这是一个很大的问题,我认为还有很多人比我更胜任,但我会提供一些初步指导.

在Software Foundations(一本关于Coq的书)中,他们谈论了一种称为Imp的隐含语言. Imp的语法如下:

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

应该容易理解为赋值和一些简单的循环. ::=用于赋值,一个while循环直到z为0.在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-当前/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