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에 관한 책인 Software Foundations에서 그들은 Imp라는 묵시적 언어에 대해 이야기합니다. Imp에는 다음과 같은 구문이 있습니다.

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

할당 및 간단한 반복으로 다소 쉽게 이해되어야합니다. ::=는 할당을위한 것이고,z가 0이 될 때까지 while 루프입니다. 파이썬에서 이것은 다음과 같습니다 :

 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으로 컴파일 할 가능성도 있지만,그것은 가능성 일 뿐이며 그 구성에 대한 증거를 보지 못했습니다.

참조 : 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