Abstract Many compilation stages of smart contracts on the Ethereum blockchain have been transitioned to the intermediate language . Tasks such as smart contract optimization and bytecode generation are—or will soon be—performed directly at the level in the compilers for the higher-level languages such as Solidity. In this paper, we develop a formal semantics of programs in Rocq, suitable for verification, which allows formal reasoning at the level of code or generation tools processing programs. Our semantics is expressive enough to be the basis for formal verification tools, and simple enough to make the development of such tools feasible. In order to prove its adequacy for verification, we develop in Rocq a checker (and associated soundness proofs), based on our semantics, able to verify the results of the liveness analysis stage of the official Solidity compiler , which opens the door towards formally verified Ethereum’s smart contracts compilation. Experiments on more than 1,500 smart contracts show that we are able to automatically verify ’s liveness analysis results in negligible time.

Program optimization is a key factor for green software. In the context of the Ethereum blockchain, optimization is particularly relevant because there is a fee to pay for each EVM (Ethereum Virtual Machine) instruction executed and also there exist bytecode-size limitations for deploying the software on the blockchain. Still, optimization of EVM code is not as widely spread as one could imagine. This is at least partly due to the lack of trust in the correctness of the tools, as security is even more relevant than efficiency in the blockchain context in which bugs may cause huge economical losses. This article develops a formal verification framework using Coq to ensure the security of EVM optimizations performed on jump-free sequences of EVM bytecode. By means of Coq’s theorem proving capabilities, we are able to automatically verify/certify that an optimized jump-free sequence of EVM opcodes is semantically equivalent to a given original one. We also present an extension to our framework that can handle inter-block optimizations that propagate global information across blocks. We have applied our tool to successfully prove the security of peephole optimizations performed by the standard Solidity compiler, and also to existing EVM superoptimization tools (namely GASOL and Superstack) in which we have found bugs that have been reported and fixed.

Abstract The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations , which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two blocks under comparison. Artifact: https://doi.org/10.5281/zenodo.7863483

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused to build robots with autonomous navigation capabilities. This library is a critical component, as navigation failures could have catastrophic consequences for applications like self-driving cars where safety is crucial. Here we devise a general methodology for verifying this kind of complex systems by specifying them in different executable specification languages with verification support and validating the equivalence between the specifications and the original system using differential testing techniques. The complex system can then be indirectly analyzed using the verification tools of the specification languages like model checking, semi-automated functional verification based on Hoare logic, and other formal techniques. In this paper we apply this verification methodology to the NavFn planner, which is the main planner component of the Navigation Stack of ROS, using Maude and Dafny as specification languages. We have formally proved several desirable properties of this planner algorithm like the absence of obstacles in the planned path. Moreover, we have found counterexamples for other concerns like the optimality of the path cost.

Databases are a key subject in several technical degrees.Because they have a strong practical nature, students require a large number of problems to master them.However, these problems are useful only if accurate and timely feedback is provided.In this paper, we present the learning improvements obtained by using LearnSQL, an automatic judge that has been designed to complement face-to-face lectures.We have measured the impact of this judge during the 2021/22 academic year and report promising results both in student engagement and final grades.

Abstract This paper presents a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. As in previous approaches, the analysis searches for a metering function that under-approximates the number of loop iterations. The key novelty of our framework is the specialization of loops, which is achieved by restricting their enabled transitions to a subset of the inputs combined with the narrowing of their transition scopes. Specialization allows us to find metering functions for complex loops that could not be handled before or be more precise than previous approaches. Technically, it is performed (1) by using quasi-invariants while searching for the metering function, (2) by strengthening the loop guards, and (3) by narrowing the space of non-deterministic choices. We also propose a Max-SMT encoding that takes advantage of the use of soft constraints to force the solver look for more accurate solutions. We show our accuracy gains on benchmarks extracted from the 2020 Termination and Complexity Competition by comparing our results to those obtained by the "Image missing" system.

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

Abstract In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, and imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice.

Abstract When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools.

This article presents a may-happen-in-parallel (MHP) analysis for languages with actor-based concurrency . In this concurrency model, actors are the concurrency units such that, when a method is invoked on an actor a 2 from a task executing on actor a 1 , statements of the current task in a 1 may run in parallel with those of the (asynchronous) call on a 2 , and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level ( local ) analysis whose information can be modularly composed to obtain application-level ( global ) information. The information yielded by the MHP analysis is essential to infer more complex properties of actor-based concurrent programs, for example, data race detection, deadlock freeness, termination, and resource consumption analyses can greatly benefit from the MHP relations to increase their accuracy. We report on MayPar, a prototypical implementation of an MHP static analyzer for a distributed asynchronous language.

We propose a new type system for functional logic programming which is more liberal than the classical Damas–Milner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from Damas–Milner typing of expressions, we propose a new notion of well-typed program that adds support for type-indexed functions, a particular form of existential types, opaque higher-order patterns and generic functions – as shown by an extensive collection of examples that illustrate the possibilities of our proposal. In the negative side, the types of functions must be declared, and therefore types are checked but not inferred. Another consequence is that parametricity is lost, although the impact of this flaw is limited as ‘free theorems’ were already compromised in functional logic programming because of non-determinism.

Abstract Non-confluent and non-terminating {constructor-based term rewriting systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kinds of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism iscall-time choice, whose combination with non-strictness is a non-trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper, we develop thoroughly the theory for the first-order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing, which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense.

We present a transformational approach to type inference for functional logic programs. More concretely, we give a broad set of examples showing how, given a functional logic program P, we can synthesize a remarkably simple and natural functional logic program P' such that the evaluation of expressions with respect to P' corresponds to typing the expressions in the original P. We start developing those ideas for the case of type inference with standard Hindley-Milner types, and after that we consider some variations, like local definitions with different degrees of polymorphism, existential types and type checking in the presence of polymorphic recursion. For the basic case of Hindley-Milner types we provide also a formalization of the transformation and proofs of its correctness. Besides its potential applicability to the implementation of different type systems, or to the educational use of the synthesized typing programs to explain different type inference/checking processes, the paper demonstrates vividly the expressive power of functional logic languages, as well as some of their limitations for metaprogramming purposes, that we have overcome by providing a suitable set of metalogical functions to inspect, classify and manipulate expressions according to their structure, similar to well known Prolog metapredicates for such purposes.

Narrowing is the usual computation mechanism in functional-logic programming (FLP), where bindings for free variables are found at the same time that expressions are reduced. These free variables may be already present in the goal expression, but they can also be introduced during computations by the use of program rules with extra variables. However, it is known that narrowing in FLP generates problems from the point of view of types, problems that can only be avoided using type information at run-time. Nevertheless, most FLP systems use static typing based on Damas-Milner type system and they do not carry any type information in execution, thus ill-typed reductions may be performed in these systems. In this paper we prove, using the let-narrowing relation as the operational mechanism, that types are preserved in narrowing reductions provided the substitutions used preserve types. Based on this result, we prove that types are also preserved in narrowing reductions without type checks at run-time when higher order (HO) variable bindings are not performed and most general unifiers are used in unifications, for programs with transparent patterns. Then we characterize a restricted class of programs for which no binding of HO variables happens in reductions, identifying some problems encountered in the definition of this class. To conclude, we use the previous results to show that a simulation of needed narrowing via program transformation also preserves types.

Functional logic programming (FLP) is a paradigm that comes from the integration of lazy functional programming and logic programming. Although most FLP systems use static typing by means of a direct adaptation of Damas-Milner type system, it is well-known that some FLP features like higher-order patterns or the equality operator lead to so-called opacity situations that are not properly handled by Damas-Milner type system, thus leading to the loss of type preservation. Previous works have addressed this problem either directly forbidding those HO patterns that are opaque or restricting its use. In this paper we propose a new approach that is based on eliminating the unintended opacity created by HO patterns and the equality operator by extending the expressiveness of the type language with decorations in the arrows of the functional types. We study diverse possibilities, which differ in the amount of information included in the decorations. The obtained type systems have different properties and expressiveness, but each of them recovers type preservation from simple extensions of Damas-Milner.

Type classes provide a clean, modular and elegant way of writing overloaded functions. Functional logic programming languages (FLP in short) like Toy or Curry have adopted the Damas-Milner type system, so it seems natural to adopt also type classes in FLP. However, type classes has been barely introduced in FLP. A reason for this lack of success is that the usual translation of type classes using dictionaries presents some problems in FLP like the absence of expected answers due to a bad interaction of dictionaries with the call-time choice semantics for non-determinism adopted in FLP systems.