Verifica formale degli smart contract Tezos

Se siamo d'accordo sulfatto che lo scopo dell'analisi è sia di dimostrare leproprietà sia di aiutaregli utenti di contrattiintelligenti a comprenderle,direi:

1. Valori: studio dei valori che ognielemento dello storagepuò assumerein futuro.
2. Effetti: studio deglieffetti chepossono verificarsiin futuro:in genere qualitrasferimentipossono verificarsie in quali condizioni.
3. Proprietà: chipuò attivare unamodifica su qualeparte dello spazio di archiviazione.

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.

Quindi questa è una domandaenormee penso che ci sianomoltepersonepiù qualificate dime,ma offrirò alcuneindicazioniiniziali.

In Software Foundations,un libro su Coq,parlano di un linguaggioimplicito chiamato Imp. Imp ha una sintassi come:

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

Che dovrebbeesserein qualchemodofacilmente compreso come assegnazionee alcuni semplici cicli. ::= èper l'assegnazione,un ciclo whilefinché znon è 0. Inpython questo sarebbe:

  deffoo (x):
    z=x
    y=1
 mentre z!=0:
        y=y * z
        z -=1
 

Possiamo quindi definire alcune delle logiche sottostanti ai simboli. Adesempio,

  Fixpoint aeval (a: aexp):nat:=
  abbinare a con
 | ANumn ⇒n
 | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
 | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
 | AMult a1 a2 ⇒ (aeval a1) * (aeval a2)
 fine.
 

Questo definirà le operazioni aritmetiche.

Puoi anche analizzareparole riservate,come:

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

Quindipotrestimappareilprogramma a questitipi definitiin Coq,come:

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

Possiamo quindifare alcuneprove sullefunzioni o affermazionifattein questo linguaggio usando la logicaformale. Ecco unesempio che dimostra che se znon è 4,allora xnon è 2:

  Esempio ceval_example1:
 empty_st=[
     X ::=2 ;;
     PROVA X ≤ 1
       ALLORA Y ::=3
       ALTRO Z ::=4
     FI
  ] ⇒ (Z! - > 4; X! - > 2).
Prova.
  (* Dobbiamofornire lo statointermedio *)
  applica E_Seq con (X! - > 2).
  - (* comando di assegnazione *)
    applica E_Ass. riflessività.
  - (* se comando *)
    applica E_IfFalse.
    riflessività.
    applica E_Ass. riflessività.
Qed.
 

A questopunto spero che l'applicazione a uno smart contract siain qualchemodoevidente. Sepotessi astrarre lo smart contractin Coq,potresti usare Coqper dimostrare rigorosamente alcuni componenti deltuo smart contract. C'è ancheilpotenzialeper delineare le condizioni di un contrattointelligentein Coqe compilarloper Michelson,ma questa è solo unapossibilitàe non ho visto alcunaprova della sua costruzione.

rif: 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