Recently in a private discussion forum, there was a topic under consideration which went something like this:

In pure lambda calculus (untyped or typed) the fix combinator is used to encode recursion. fix represents the least fixed point of a function f i.e the least defined x for which f x = x. An important concept is that a function need not have a least fixed point. But for those functions which do, the least fixed point is the base case for recursion. An intuition about the least fixed point is :

In this post I attempt to summarize my understandings about the transactional nature of Smart contract execution. I conducted this study, while trying to understand the DAO exploit. The basis of the DAO exploit is a recursive(or rather reentrant) message call. One important point to note that an exception(during a message call or otherwise) in the Ethereum Virtual Machine , would imply reverting all changes to state and balance. Solidity has a documentation on cases where exceptions are thrown automatically. However in certain cases like send we need to manually raise an exception using throw. So, the attacker has to be careful not to hit any exceptions while attempting the reentrant call to avoid reverting. I also rectify certain mistaken assumptions, I made in my previous post.

In this post and the coming ones, I will be detailing about a particularly interesting analogy between Smart Contracts and Transactional memory. And how we can use one to verify and reason about the other. The majority of this work has been driven by a paper by Dr. Ilya Sergey and Dr. Aquinas Hobor on similar grounds. My attempt has been to try and extend the ideas from this paper, to mitigate the issues plaguing Smart contracts and their semantics as listed in another paper on Making Smart Contracts Smarter. Essentially this serves as a literature survey as well as a playground for me to pitch my ideas unifying the 2 papers. Sounds interesting? Then read ahead. :)

A power set is simply defined as all the subsets of a set.