Following Hoare's seminal invention, later called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic.

The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions.

This paper extends the previous paper [6] by implementing two blockchain simulators of Solidity-style smart contracts - a simple and a complex one, using the interactive theorem prover Agda. In the previous article [6], we built a simple and complex abstract model of Solidity-style smart contracts in Agda. These models had many features, such as calling different smart contracts, supporting the ability to call different smart contracts, and providing simple and complex instructions. Because of the use of coalgebras for representing smart contracts they supported loops and conditionals, using the support of those features for coalgebraic programs in Agda. The complex model supported gas costs and pure functions, similar to the Solidity language. In this paper, we implement and design interfaces which allow to interactively interact with users in the simple and complex models. This makes use of the fact that Agda is as well a dependently typed programming language. Therefore we can write interactive programs which are running in the same language in which we will in a future next step verify smart contracts, avoiding the translation of programs which could be a source of errors. The simple blockchain simulator we have created can call other contracts, transfer funds to specific contracts, and update contracts. The complex blockchain simulator has in addition features that can deal with more complex blockchain instructions, support gas costs, and evaluate and update pure functions.

This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Lof type theory. In this paper, we overcome the obstacle of not having direct access to untyped terms in Martin-Lof type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Lof type theory with certain indexed inductive-recursive definitions. In this way, we can relate the predicativity question to the fundamental semantics of Martin-Lof type theory in terms of computation to canonical form. As a result, we get the first extended predicative definition of a Mahlo universe in Martin-Lof type theory. To this end, we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Lof type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory $\mathbf {IIRD}$ of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Lof's sense. The model construction has been type-checked in the proof assistant Agda.

We consider the structures (Z; SF), (Z;<, SF), (Q; SF), and (Q;<, SF) where Z is the additive group of integers, SF is the set of a ∈ Z such that vp(a) < 2 for every prime p and corresponding p-adic valuation vp , Q and SF are defined likewise for rational numbers, and < denotes the natural ordering on each of these domains. We prove that the second structure is model-theoretically wild while the other three structures are model-theoretically tame. Moreover, all these results can be seen as examples where number-theoretic randomness yields model-theoretic consequences. §

In this paper, we specify and verify the correctness of programs written in Bitcoin's smart contract SCRIPT in the interactive theorem prover Agda. As in the previous article [1], we use weakest preconditions of Hoare logic to specify the security property of access control, and show how to develop human-readable specifications. In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if- and else-case.

This paper contributes to the verification of programs written in Bitcoin's smart contract language SCRIPT in the interactive theorem prover Agda. It focuses on the security property of access control for SCRIPT programs that govern the distribution of Bitcoins. It advocates that weakest preconditions in the context of Hoare triples are the appropriate notion for verifying access control. It aims at obtaining human-readable descriptions of weakest preconditions in order to close the validation gap between user requirements and formal specification of smart contracts. As examples for the proposed approach, the paper focuses on two standard SCRIPT programs that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). The paper introduces an operational semantics of the SCRIPT commands used in P2PKH and P2MS, which is formalised in the Agda proof assistant and reasoned about using Hoare triples. Two methodologies for obtaining human-readable descriptions of weakest preconditions are discussed: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes grouping several instructions together; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of conjunctions of conditions along accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda. Keywords and phrases: Blockchain; Cryptocurrency; Bitcoin; Agda; Verification; Hoare logic; Bitcoin script; P2PKH; P2MS; Access control; Weakest precondition; Predicate transformer semantics; Provable correctness; Symbolic execution; Smart contracts

An abstract is not available for this content so a preview has been provided. As you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The following is not very well checked yet, i.e. there might be some typoi and mistakes.

We present an upper bound for the proof theoretic strength of Martin-Lof’s type theory with W-type and one universe. This proof, together with the well ordering proof carried out in [12] shows that the proof theoretic strength of this theory is precisely ψΩ1ΩI+ω, which is slightly more than the strength of Feferman’s theory T0, the classical set theory KPI, and the subsystem of analysis (Δ12−CA)+(BI). The strength of the intensional and extensional version, and of the version a la Tarski and a la Russell are shown to be the same. The proof is carried out by interpreting the type theories in question in an extension of Kripke-Platek set theory KPI+. We show that validity of Π11-sentences is preserved in this interpretation.

We present two models of the block chain of Bitcoin in the interactive theorem prover Agda. The first one is based on a simple model of bank accounts, while having transactions with multiple inputs and outputs. The second model models transactions, which refer directly to unspent transaction outputs, rather than user accounts. The resulting blockchain gives rise to a transaction tree. That model is formalised using an extended form of induction-recursion, one of the unique features of Agda. The set of transaction trees and transactions is defined inductively, while simultaneously recursively defining the list of unspent transaction outputs. Both structures model standard transactions, coinbase transactions, transaction fees, the exact message to be signed by those spending money in a transaction, block rewards, blocks, and the blockchain, and the second structure models as well maturation time for coinbase transactions and Merkle trees. Hashing and cryptographic operations and their correctness are dealt with abstractly by postulating corresponding operations. An indication is given how the correctness of this model could be specified and proven in Agda.

We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.

Decidability of type checking for dependently typed languages usually requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one cannot use it as the equality in type checking. Instead, languages based on dependent types with decidable type checking such as Coq or Agda use intensional equality for type checking. Two streams are definitionally equal if the underlying terms reduce to the same normal form, i.e. if the underlying programs are syntactically equivalent. For reasoning about equality of streams one introduces bisimilarity as a propositional rather than judgemental equality.