Формальная проверка смарт-контрактов 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 и скомпилировать их для Майкельсона,но это всего лишь возможность,и я не видел никаких доказательств его построения.

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