Clean-up of the white-listing

io-hotmoka-instrumentation/src/main/java/io/hotmoka/instrumentation/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java

@@ -392,7 +392,7 @@ private InvokeInstruction addWhiteListVerificationMethodForNonINVOKEDYNAMIC(Inst
 		il.append(invoke);
 		il.append(InstructionFactory.createReturn(verifierReturnType));
 
-		Type[] argsAsArray = args.toArray(Type[]::new);
+		var argsAsArray = args.toArray(Type[]::new);
 		var addedVerifier = new MethodGen(PRIVATE_SYNTHETIC_STATIC, verifierReturnType, argsAsArray, null, verifierName, className, il, cpg);
 		addMethod(addedVerifier, false);
 

io-hotmoka-tests/src/test/java/io/hotmoka/tests/HotmokaTest.java

@@ -152,11 +152,11 @@ public void beforeAll(ExtensionContext context) throws Exception {
 	    		privateKeyOfGamete = keys.getPrivate();
 
 	    		Node wrapped;
-	    		//node = wrapped = mkDiskNode();
+	    		node = wrapped = mkDiskNode();
 	    		//node = wrapped = mkMokamintNodeConnectedToPeer();
 	    		//node = wrapped = mkMokamintNetwork(4);
 	    		//node = wrapped = mkTendermintNode();
-	    		node = mkRemoteNode(wrapped = mkDiskNode());
+	    		//node = mkRemoteNode(wrapped = mkDiskNode());
 	    		//node = mkRemoteNode(wrapped = mkMokamintNetwork(1));
 	    		//node = mkRemoteNode(wrapped = mkTendermintNode());
 	    		//node = wrapped = mkRemoteNode("ec2-54-194-239-91.eu-west-1.compute.amazonaws.com:8080");

io-hotmoka-tests/src/test/java/io/hotmoka/tests/errors/LegalStaticInitialization1.java

@@ -16,20 +16,12 @@
 
 package io.hotmoka.tests.errors;
 
-import java.io.IOException;
 import java.math.BigInteger;
-import java.security.InvalidKeyException;
-import java.security.SignatureException;
-import java.util.NoSuchElementException;
-import java.util.concurrent.TimeoutException;
 
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.DisplayName;
 import org.junit.jupiter.api.Test;
 
-import io.hotmoka.node.api.NodeException;
-import io.hotmoka.node.api.TransactionException;
-import io.hotmoka.node.api.TransactionRejectedException;
 import io.hotmoka.tests.HotmokaTest;
 
 class LegalStaticInitialization1 extends HotmokaTest {
@@ -40,7 +32,7 @@ void beforeEach() throws Exception {
 	}
 
 	@Test @DisplayName("install jar")
-	void installJar() throws TransactionException, IOException, TransactionRejectedException, InvalidKeyException, SignatureException, NoSuchElementException, NodeException, TimeoutException, InterruptedException {
+	void installJar() throws Exception {
 		addJarStoreTransaction(privateKey(0), account(0), _500_000, BigInteger.ONE, takamakaCode(), bytesOf("legalstaticinitialization1.jar"), takamakaCode());		
 	}
 }

io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/UnsupportedVerificationVersionException.java

@@ -19,8 +19,8 @@
 /**
  * An exception thrown when the verification version of the node is not supported.
  */
+@SuppressWarnings("serial")
 public class UnsupportedVerificationVersionException extends Exception {
-	private static final long serialVersionUID = -1232455923178336022L;
 
 	/**
 	 * The unsupported verification version.

io-hotmoka-whitelisting-api/src/main/java/io/hotmoka/whitelisting/api/WhiteListingProofObligation.java

@@ -23,7 +23,7 @@
 import java.lang.annotation.Target;
 
 /**
- * States that an annotation is meant to decorate an argument of a method
+ * An annotation that is meant to decorate an argument of a method
  * or constructor of a white-listed method and specifies some property that
  * the argument must satisfy, for the method to be white-listed.
  */

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryCollection.java

@@ -0,0 +1,39 @@
+/*
+Copyright 2021 Fausto Spoto
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+*/
+
+package io.hotmoka.whitelisting;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Inherited;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+import io.hotmoka.whitelisting.api.WhiteListingProofObligation;
+import io.hotmoka.whitelisting.internal.checks.MustBeSafeLibraryCollectionCheck;
+
+/**
+ * States that an object of a white-listed method must be a safe library collection,
+ * exactly, hence not a user-defined collection class.
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target(value={ ElementType.METHOD, ElementType.PARAMETER })
+@Inherited
+@Documented
+@WhiteListingProofObligation(check = MustBeSafeLibraryCollectionCheck.class)
+public @interface MustBeSafeLibraryCollection {
+}

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/MustBeSafeLibraryMap.java

@@ -0,0 +1,39 @@
+/*
+Copyright 2021 Fausto Spoto
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+*/
+
+package io.hotmoka.whitelisting;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Inherited;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+import io.hotmoka.whitelisting.api.WhiteListingProofObligation;
+import io.hotmoka.whitelisting.internal.checks.MustBeSafeLibraryMapCheck;
+
+/**
+ * States that an object of a white-listed method must be a safe library map,
+ * exactly, hence not a user-defined map class.
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target(value={ ElementType.METHOD, ElementType.PARAMETER })
+@Inherited
+@Documented
+@WhiteListingProofObligation(check = MustBeSafeLibraryMapCheck.class)
+public @interface MustBeSafeLibraryMap {
+}

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsAndHashCodeCheck.java

@@ -73,23 +73,23 @@ private static boolean hashCodelsIsDeterministicAndTerminating(Class<?> clazz, W
 
 	private static Optional<Method> getHashCodeFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "hashCode".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 0
-						&& "hashCode".equals(method.getName())
 						&& method.getReturnType() == int.class)
 				.findFirst();
 	}
 
 	private static Optional<Method> getEqualsFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "equals".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 1
 						&& method.getParameterTypes()[0] == Object.class
-						&& "equals".equals(method.getName())
 						&& method.getReturnType() == boolean.class)
 				.findFirst();
 	}

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingEqualsCheck.java

@@ -45,8 +45,7 @@ private static boolean equalsIsDeterministicAndTerminating(Class<?> clazz, White
 	}
 
 	private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) {
-		Optional<Method> model = wizard.whiteListingModelOf(method);
-		return model.isPresent() && hasNoProofObligations(model.get());
+		return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingEqualsCheck::hasNoProofObligations).orElse(false);
 	}
 
 	private static boolean hasNoProofObligations(Method model) {
@@ -59,12 +58,12 @@ private static boolean hasNoProofObligations(Method model) {
 
 	private static Optional<Method> getEqualsFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "equals".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 1
 						&& method.getParameterTypes()[0] == Object.class
-						&& "equals".equals(method.getName())
 						&& method.getReturnType() == boolean.class)
 				.findFirst();
 	}

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingHashCodeCheck.java

@@ -33,17 +33,15 @@ public class HasDeterministicTerminatingHashCodeCheck implements WhiteListingPre
 
 	@Override
 	public boolean test(Object value, WhiteListingWizard wizard) {
-		return value == null || hashCodelsIsDeterministicAndTerminating(value.getClass(), wizard);
+		return value == null || hashCodeIsDeterministicAndTerminating(value.getClass(), wizard);
 	}
 
-	private static boolean hashCodelsIsDeterministicAndTerminating(Class<?> clazz, WhiteListingWizard wizard) {
-		Optional<Method> hashCode = getHashCodeFor(clazz);
-		return hashCode.isPresent() && isInWhiteListingDatabaseWithoutProofObligations(hashCode.get(), wizard);
+	private static boolean hashCodeIsDeterministicAndTerminating(Class<?> clazz, WhiteListingWizard wizard) {
+		return getHashCodeFor(clazz).map(hashCode -> isInWhiteListingDatabaseWithoutProofObligations(hashCode, wizard)).orElse(false);
 	}
 
 	private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) {
-		Optional<Method> model = wizard.whiteListingModelOf(method);
-		return model.isPresent() && hasNoProofObligations(model.get());
+		return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingHashCodeCheck::hasNoProofObligations).orElse(false);
 	}
 
 	private static boolean hasNoProofObligations(Method model) {
@@ -56,11 +54,11 @@ private static boolean hasNoProofObligations(Method model) {
 
 	private static Optional<Method> getHashCodeFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "hashCode".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 0
-						&& "hashCode".equals(method.getName())
 						&& method.getReturnType() == int.class)
 				.findFirst();
 	}

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/HasDeterministicTerminatingToStringCheck.java

@@ -33,19 +33,18 @@ public class HasDeterministicTerminatingToStringCheck implements WhiteListingPre
 
 	@Override
 	public boolean test(Object value, WhiteListingWizard wizard) {
-		return value == null || toStringlsIsDeterministicAndTerminating(value.getClass(), wizard);
+		return value == null || toStringIsDeterministicAndTerminating(value.getClass(), wizard);
 	}
 
-	private static boolean toStringlsIsDeterministicAndTerminating(Class<?> clazz, WhiteListingWizard wizard) {
+	private static boolean toStringIsDeterministicAndTerminating(Class<?> clazz, WhiteListingWizard wizard) {
 		Optional<Method> toString = getToStringFor(clazz);
 		return toString.isPresent() &&
 				(isInWhiteListingDatabaseWithoutProofObligations(toString.get(), wizard)
 						|| toStringIsInObjectAndHashCodeIsDeterministicAndTerminating(toString.get(), clazz, wizard));
 	}
 
 	private static boolean isInWhiteListingDatabaseWithoutProofObligations(Method method, WhiteListingWizard wizard) {
-		Optional<Method> model = wizard.whiteListingModelOf(method);
-		return model.isPresent() && hasNoProofObligations(model.get());
+		return wizard.whiteListingModelOf(method).map(HasDeterministicTerminatingToStringCheck::hasNoProofObligations).orElse(false);
 	}
 
 	private static boolean hasNoProofObligations(Method model) {
@@ -58,33 +57,28 @@ private static boolean hasNoProofObligations(Method model) {
 
 	private static Optional<Method> getToStringFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "toString".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 0
-						&& "toString".equals(method.getName())
 						&& method.getReturnType() == String.class)
 				.findFirst();
 	}
 
 	private static Optional<Method> getHashCodeFor(Class<?> clazz) {
 		return Stream.of(clazz.getMethods())
-				.filter(method -> !Modifier.isAbstract(method.getModifiers())
+				.filter(method -> "hashCode".equals(method.getName())
+						&& !Modifier.isAbstract(method.getModifiers())
 						&& Modifier.isPublic(method.getModifiers())
 						&& !Modifier.isStatic(method.getModifiers())
 						&& method.getParameters().length == 0
-						&& "hashCode".equals(method.getName())
 						&& method.getReturnType() == int.class)
 				.findFirst();
 	}
 
 	private static boolean toStringIsInObjectAndHashCodeIsDeterministicAndTerminating(Method toString, Class<?> clazz, WhiteListingWizard wizard) {
-		if (toString.getDeclaringClass() == Object.class) {
-			Optional<Method> hashCode = getHashCodeFor(clazz);
-			return hashCode.isPresent() && isInWhiteListingDatabaseWithoutProofObligations(hashCode.get(), wizard);
-		}
-		else
-			return false;
+		return toString.getDeclaringClass() == Object.class && getHashCodeFor(clazz).map(hashCode -> isInWhiteListingDatabaseWithoutProofObligations(hashCode, wizard)).orElse(false);
 	}
 
 	@Override

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeFalseCheck.java

@@ -26,7 +26,7 @@ public class MustBeFalseCheck implements WhiteListingPredicate {
 
 	@Override
 	public boolean test(Object value, WhiteListingWizard wizard) {
-		return value.equals(Boolean.FALSE);
+		return Boolean.FALSE.equals(value);
 	}
 
 	@Override

io-hotmoka-whitelisting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryCollectionCheck.java

@@ -0,0 +1,45 @@
+/*
+Copyright 2023 Fausto Spoto
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+*/
+
+package io.hotmoka.whitelisting.internal.checks;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.LinkedList;
+
+import io.hotmoka.whitelisting.api.WhiteListingPredicate;
+import io.hotmoka.whitelisting.api.WhiteListingWizard;
+
+/**
+ * A check that the class of a value is exactly one of the allowed collection classes from the library
+ * (not a user subclass then).
+ */
+public class MustBeSafeLibraryCollectionCheck implements WhiteListingPredicate {
+
+	@Override
+	public boolean test(Object value, WhiteListingWizard wizard) {
+		return value == null || isSafeLibraryCollection(value.getClass());
+	}
+
+	private static boolean isSafeLibraryCollection(Class<?> clazz) {
+		return clazz == HashSet.class || clazz == LinkedList.class || clazz == ArrayList.class;
+	}
+
+	@Override
+	public String messageIfFailed(String methodName) {
+		return "cannot prove that this object is a safe library collection";
+	}
+}