Semantic Understanding of Smart Contracts Executable Operational Semantics of Solidity