Add an example on how to reason about events in CVL

CVLByExample/Events/README.md

@@ -0,0 +1,17 @@
+# Reasoning about Solidity events
+
+This directory demonstrates how to reason about Solidity events with the Prover. 
+The Prover cannot natively reason about events, therefore a workaround is needed.
+
+The workaround is to wrap the `emits` of Solidity `events` into an internal function and then apply internal summarization to reason about the emitted event. 
+
+See `contracts/Auction.sol` for the original code that uses an event and take a look at `contract/AuctionFixed.sol` for code that uses the workaround.
+
+- 
+Run this configuration via:
+
+```certoraRun runAuctionFixed.conf```
+
+[A report of this run](https://prover.certora.com/output/53900/4ffdad0c20094a729d830bfb1b460f3e?anonymousKey=b345ea4d1fe4b3631442c0f110e926a58f47ee9b)
+
+

CVLByExample/Events/certora/specs/Auction.spec

@@ -0,0 +1,37 @@
+/**
+ * @title  Reasoning about Solidity events example
+ *
+ * This is an example specification for reasoning about events in CVL.
+ */
+
+methods {
+    function emitBidEvent(address from) internal => cvlEmitBidEvent(from); 
+}
+
+persistent ghost bool isEventEmitted;
+persistent ghost address emittedEventAddress;
+
+function cvlEmitBidEvent(address from){
+    isEventEmitted = true;
+    emittedEventAddress = from;
+}
+
+/**
+ * This rule checks that an event is emitted
+ */
+rule eventIsEmitted() {
+    env e;
+    isEventEmitted = false;
+    bid(e);
+    assert isEventEmitted;
+}
+
+/**
+ * This rule checks that the emitted event address is the one
+ * that initiated the bid operation. 
+ */
+rule eventEmitsMsgSender() {
+    env e;
+    bid(e);
+    assert emittedEventAddress == e.msg.sender;
+}

CVLByExample/Events/contracts/Auction.sol

@@ -0,0 +1,8 @@
+contract Auction 
+{
+    event BidEvent(address from);
+    function bid() public
+    {
+        emit BidEvent(msg.sender);
+    }
+}

CVLByExample/Events/contracts/AuctionFixed.sol

@@ -0,0 +1,13 @@
+contract AuctionFixed 
+{
+    event BidEvent(address from);
+    function bid() public
+    {
+        emitBidEvent(msg.sender);
+    }
+
+    function emitBidEvent(address from) internal
+    {
+        emit BidEvent(from);
+    }
+}

CVLByExample/Events/runAuctionFixed.conf

@@ -0,0 +1,8 @@
+{
+  "files": [
+    "contracts/AuctionFixed.sol",
+  ],
+  "verify": "AuctionFixed:certora/specs/Auction.spec",
+  "msg": "Reasoning about Solidity events",
+  "rule_sanity" : "basic"  // check there is a trace satisfying the rule.
+}