Programming Hotmoka
A tutorial on Hotmoka and smart contracts in Takamaka

9.3 Command-line verification and instrumentation

If a jar being installed in a Hotmoka node does not satisfy the static constraints in Sec. 9.2, the installation transaction fails with a verification exception, no jar is actually installed but the gas of the caller gets consumed. Hence it is not practical to realize that a static constraint does not hold only by trying to install a jar in a node. Instead, it is desirable to verify all constraints off-line, fix all violations (if any) and only then install the jar in the node. This is possible by using the moka command-line interface of Hotmoka. Namely, it provides a subcommand that performs the same identical jar verification that would be executed when a jar is installed in a Hotmoka node.

Create a jar file containing a wrong version of the io-hotmoka-tutorial-examples-family project. For that, copy the io-hotmoka-tutorial-examples-family project into a new project io-hotmoka-tutorial-examples-family_errors project, change the artifact name in its pom.xml into io-hotmoka-tutorial-examples-family_errors and modify its Person class so that it contains a few errors, as follows:

package io.hotmoka.tutorial.examples.family;


import io.takamaka.code.lang.Exported;
import io.takamaka.code.lang.Payable;
import io.takamaka.code.lang.Storage;
import io.takamaka.code.lang.StringSupport;


@Exported
public class Person extends Storage {
    private final String name;
    private final int day;
    private final int month;
    private final int year;


    // error: arrays are not allowed in storage
    public final Person[] parents = new Person[2];


    public static int toStringCounter;


    public Person(String name, int day, int month, int year, Person parent1, Person parent2) {
        this.name = name;
        this.day = day;
        this.month = month;
        this.year = year;
        this.parents[0] = parent1;
        this.parents[1] = parent2;
    }


    // error: @Payable without @FromContract,
    // missing amount and @Payable method not in a Contract
    public @Payable Person(String name, int day, int month, int year) {
        this(name, day, month, year, null, null);
    }


    @Override
    public String toString() {
        toStringCounter++; // error: static update (putstatic) is not allowed
        return StringSupport.concat(name, " (", day, "/", month, "/", year, ")");
    }
}

Then generate the io-hotmoka-tutorial-examples-family_errors-1.11.5.jar file and store it in the cache of Maven:

cd io-hotmoka-tutorial-examples-family_errors
mvn install

Let us start with the verification of io-takamaka-code-1.8.1.jar, that we should find in the cache of Maven:

moka jars verify ~/.m2/repository/io/hotmoka/io-takamaka-code/1.8.1/io-takamaka-code-1.8.1.jar --init

Verification succeeded

No error has been issued, since the code does not violate any static constraint. Note that we used the --init switch, since otherwise we would get many errors related to the use of the forbidden io.takamaka.code.* package. With that switch, we verify the jar as it would be verified before node initialization, that is, by considering such package as legal.

We can generate the instrumented jar, exactly as it would be generated during installation in a Hotmoka node. For that, we run:

mkdir instrumented
moka jars instrument ~/.m2/repository/io/hotmoka/io-takamaka-code/1.8.1/io-takamaka-code-1.8.1.jar instrumented/io-takamaka-code-1.8.1.jar --init

Instrumentation succeeded

The moka jars instrument command verifies and instruments the jar, and then stores its instrumented version inside the instrumented directory.

Let us verify and instrument io-hotmoka-tutorial-examples-family-1.11.5.jar now (that is, the correct version of the project). As all Takamaka programs, that jar uses classes from the io-takamaka-code jar, hence it depends on it. We specify this with the --libs option, that must refer to an already instrumented jar:

moka jars instrument ~/.m2/repository/io/hotmoka/io-hotmoka-tutorial-examples-family/1.11.5/io-hotmoka-tutorial-examples-family-1.11.5.jar instrumented/io-hotmoka-tutorial-examples-family-1.11.5.jar --libs instrumented/io-takamaka-code
-1.8.1.jar

Instrumentation succeeded

As you can see, verification succeeds this time as well and an instrumented jar file named io-hotmoka-tutorial-examples-family-1.11.5.jar appears in the instrumented directory. Note that we have not used the --init switch this time, since we wanted to simulate the verification as it would occur after the node has been already initialized, when users add their jars to the store of the node.

Let us verify the io-hotmoka-tutorial-examples-family_errors-1.11.5.jar archive now, that (we know) contains a few errors. This time, verification will fail and the errors will be printed on the screen:

moka jars verify ~/.m2/repository/io/hotmoka/io-hotmoka-tutorial-examples-family_errors/1.11.5/io-hotmoka-tutorial-examples-family_errors-1.11.5.jar --libs instrumented/io-takamaka-code-1.8.1.jar

Verification failed with the following errors:
1: io/hotmoka/tutorial/examples/family/Person.java field parents: type not allowed for a field of a storage class
2: io/hotmoka/tutorial/examples/family/Person.java method <init>: @Payable can only be applied to constructors or instance methods of a contract class or of an interface
3: io/hotmoka/tutorial/examples/family/Person.java method <init>: a @Payable method must have a first argument for the paid amount, of type int, long or BigInteger
4: io/hotmoka/tutorial/examples/family/Person.java method <init>: @Payable can only be applied to a @FromContract method or constructor
5: io/hotmoka/tutorial/examples/family/Person.java:82: static fields cannot be updated

The same failure occurs with the moka jars instrument command, that will not generate the instrumented jar. It only reports the first encountered error before failure:

moka jars instrument ~/.m2/repository/io/hotmoka/io-hotmoka-tutorial-examples-family_errors/1.11.5/io-hotmoka-tutorial-examples-family_errors-1.11.5.jar instrumented/io-hotmoka-tutorial-examples-family_errors-1.11.5.jar --libs
instrumented/io-takamaka-code-1.8.1.jar

Instrumentation failed [io.hotmoka.verification.api.VerificationException: io/hotmoka/tutorial/examples/family/Person.java field parents: type not allowed for a field of a storage class]