From 9d80d7eafbfb235f52b3e065adbc9e8ddee8176a Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Tue, 30 Jan 2024 12:43:21 +0200
Subject: [PATCH 1/9] Add ecrecover example

---
 CVLByExample/Ecrecover/Verify.sol     |  70 +++++++++
 CVLByExample/Ecrecover/ecrecover.conf |   8 ++
 CVLByExample/Ecrecover/ecrecover.spec | 196 ++++++++++++++++++++++++++
 3 files changed, 274 insertions(+)
 create mode 100644 CVLByExample/Ecrecover/Verify.sol
 create mode 100644 CVLByExample/Ecrecover/ecrecover.conf
 create mode 100644 CVLByExample/Ecrecover/ecrecover.spec

diff --git a/CVLByExample/Ecrecover/Verify.sol b/CVLByExample/Ecrecover/Verify.sol
new file mode 100644
index 00000000..7e181f63
--- /dev/null
+++ b/CVLByExample/Ecrecover/Verify.sol
@@ -0,0 +1,70 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// game developer depoloys contract
+contract Verify {
+
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external  returns (bool) {
+        return ecrecover(msgHash, v, r, s) == _addr;
+    }
+
+
+mapping (address => uint256) private nonces; 
+
+function executeMyFunctionFromSignature(
+    uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) external {
+
+    bytes32 hash = getHash(owner, myParam, deadline);
+
+    
+    address signer = ecrecover(hash, v, r, s);
+    require(signer == owner, "MyFunction: invalid signature");
+    require(signer != address(0), "ECDSA: invalid signature");
+
+    require(block.timestamp < deadline, "MyFunction: signed transaction expired");
+    nonces[owner]++;
+
+    _myFunction(owner, myParam);
+}
+
+function _myFunction(address owner, uint256 myParam) internal {
+
+}
+
+function getHash(
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) public returns(bytes32) {
+    bytes32 eip712DomainHash = keccak256(
+        abi.encode(
+            keccak256(
+                "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"
+            ),
+            keccak256(bytes("MyContractName")),
+            keccak256(bytes("1")),
+            address(this)
+        )
+    );
+
+    bytes32 hashStruct = keccak256(
+        abi.encode(
+            keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"),
+            owner,
+            myParam,
+            nonces[owner],
+            deadline
+        )
+    );
+
+    return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct));
+}
+
+
+}
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/ecrecover.conf b/CVLByExample/Ecrecover/ecrecover.conf
new file mode 100644
index 00000000..27544cee
--- /dev/null
+++ b/CVLByExample/Ecrecover/ecrecover.conf
@@ -0,0 +1,8 @@
+{
+    "files": [
+        "Verify.sol"
+    ],
+    "optimistic_hashing": true,
+    "rule_sanity": "advanced", 
+    "verify": "Verify:ecrecover.spec"
+}
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
new file mode 100644
index 00000000..a9e0bd92
--- /dev/null
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -0,0 +1,196 @@
+/***
+This example explains many features of Certora Verification Language. 
+See https://docs.certora.com for a complete guide.
+
+Example for ecrecover 
+***/
+
+/*
+    Declaration of methods that are used in the rules. envfree indicate that
+    the method is not dependent on the environment (msg.value, msg.sender).
+    Methods that are not declared here are assumed to be dependent on env.
+*/
+
+
+/*** # ecrecover properties:
+# 1. zero value:
+        ecrecover(0, v, r, s) == 0
+# 2. deterministic 
+        ecrecover(msgHash, v, r, s) == _addr on different calls.  
+# 3. uniqueness of signature
+        ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash', v, r, s) == 0
+        where msgHash' != msgHash
+# 4. Dependency on r and s
+        ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r', s) == 0
+        where r' != r
+        ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r, s') == 0
+        where s' != s
+**/
+
+
+
+methods {
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) envfree;
+    function executeMyFunctionFromSignature(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParam, uint256 deadline) external;
+    function getHash(address owner, uint256 myParam, uint256 deadline) external returns(bytes32) envfree;
+}
+
+
+function ecrecoverAxioms() {
+  // zero value:
+  require (forall uint8 v. forall bytes32 r. forall bytes32 s. ecrecover(to_bytes32(0), v, r, s) == 0);
+  // uniqueness of signature
+  require (forall uint8 v. forall bytes32 r. forall bytes32 s. forall bytes32 h1. forall bytes32 h2.
+    h1 != h2 => ecrecover(h1, v, r, s) != 0 => ecrecover(h2, v, r, s) == 0);
+  // dependency on r and s
+  require (forall bytes32 h. forall uint8 v. forall bytes32 s. forall bytes32 r1. forall bytes32 r2.
+    r1 != r2 => ecrecover(h, v, r1, s) != 0 => ecrecover(h, v, r2, s) == 0);
+  require (forall bytes32 h. forall uint8 v. forall bytes32 r. forall bytes32 s1. forall bytes32 s2.
+    s1 != s2 => ecrecover(h, v, r, s1) != 0 => ecrecover(h, v, r, s2) == 0);
+}
+
+/*
+    shows that ecrecover has a single value, i.e two different addresses can not be the result of ecrecover(msgHash, v, r, s)  
+*/
+rule zeroValue() {
+    ecrecoverAxioms();
+    bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; 
+    assert ecrecover(to_bytes32(0), v, r, s ) == 0;
+}
+
+
+
+
+rule deterministic() {
+    ecrecoverAxioms();
+    bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; 
+    assert ecrecover(msgHash, v, r, s ) == ecrecover(msgHash, v, r, s );
+}
+
+rule uniqueness() {
+    ecrecoverAxioms();
+    bytes32 msgHashA; bytes32 msgHashB; uint8 v; bytes32 r; bytes32 s; 
+    require msgHashA != msgHashB;  
+    assert ecrecover(msgHashA, v, r, s) != 0 => ecrecover(msgHashB, v, r, s) == 0;
+}
+
+rule dependencyOnS() {
+    ecrecoverAxioms();
+    bytes32 msgHash;  uint8 v; bytes32 r; bytes32 s1; bytes32 s2; 
+    require s1 != s2;  
+    assert ecrecover(msgHash, v, r, s1) != 0 => ecrecover(msgHash, v, r, s2) == 0;
+    //!= ecrecover(msgHash, v, r, s1) ;
+}
+
+rule dependencyOnR() {
+    ecrecoverAxioms();
+    bytes32 msgHash; uint8 v; bytes32 r1; bytes32 r2; bytes32 s; 
+    require r1 != r2;  
+    assert ecrecover(msgHash, v, r1, s) != 0 => ecrecover(msgHash, v, r2, s) == 0 ;
+}
+
+// Rules for a function that checks signature 
+
+rule singleVerifier () 
+{
+    ecrecoverAxioms();
+    bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; 
+    address addr1; 
+    address addr2; 
+    require addr1 != addr2 && addr1!=0 && addr2!=0 ;
+    assert isSigned(addr1, msgHash, v, r, s ) => !isSigned(addr2, msgHash, v, r, s ) ;
+
+}
+
+
+rule ownerSignatureIsUnique () {
+    ecrecoverAxioms();
+    bytes32 msgHashA; bytes32 msgHashB;
+    uint8 v; bytes32 r; bytes32 s; 
+    address addr; 
+    require msgHashA != msgHashB; 
+    require addr != 0;
+    assert isSigned(addr, msgHashA, v, r, s ) => !isSigned(addr, msgHashB, v, r, s );
+}
+
+rule hashIsUnique(
+    address ownerA,
+    uint256 myParamA,
+    uint256 deadlineA,
+    address ownerB,
+    uint256 myParamB,
+    uint256 deadlineB
+) {
+    bytes32 hashA =  getHash(ownerA, myParamA, deadlineA);
+    bytes32 hashB = getHash(ownerB, myParamB, deadlineB);
+    assert hashA == hashB => (  ownerA == ownerB && 
+                                myParamA == myParamB &&
+                                deadlineA == deadlineB ); 
+}
+
+
+/*** 
+   # High level property : there is only single owner that can be used
+    A rule which proves that for a given set of parameters only a single owner can execute .
+    This property is implemented as a relational property - it compares two different executions on the same state.
+*/
+rule onlySingleUserCanExecute(uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address alice,
+    address bob,
+    uint256 myParam,
+    uint256 deadline) {
+
+    env e1;
+    env e2;
+    ecrecoverAxioms();
+    //save the current state
+    storage init = lastStorage; 
+    //execute and assume succeeded
+    executeMyFunctionFromSignature(e1, v, r, s, alice, myParam, deadline);
+    // compare another execution on the same state, look at reverting paths
+    executeMyFunctionFromSignature@withrevert(e2, v, r, s, bob, myParam, deadline) at init;
+    bool success = !lastReverted;
+    //if it succeeded it must be the same owner, or an unrealistic hash collision
+    assert success => alice==bob ; 
+}
+
+
+/*** 
+   # High level property : params and deadline are signed 
+make sure the param and deadline are part of the signature 
+*/
+rule signedParamAndDeadline(uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParamA,
+    uint256 deadlineA,
+    uint256 myParamB,
+    uint256 deadlineB) {
+
+    env e1;
+    env e2;
+    ecrecoverAxioms();
+    //save the current state
+    storage init = lastStorage; 
+    //execute and assume succeeded
+    executeMyFunctionFromSignature(e1, v, r, s, owner, myParamA, deadlineA);
+    // compare another execution on the same state, look at reverting paths
+    executeMyFunctionFromSignature@withrevert(e2, v, r, s, owner, myParamB, deadlineB) at init;
+    bool success = !lastReverted;
+    //if it succeeded it must be the same owner, or an unrealistic hash collision
+    assert success => ( myParamA==myParamB && deadlineA == deadlineB); 
+}
+
+
+
+rule twoDifferent() {
+    ecrecoverAxioms();
+    bytes32 msgHashA;  uint8 vA; bytes32 rA; bytes32 sA; 
+    bytes32 msgHashB;  uint8 vB; bytes32 rB; bytes32 sB;
+    require  msgHashA != msgHashB;
+    require ecrecover(msgHashA, vA, rA, sA) != 0 && ecrecover(msgHashB, vB, rB, sB) != 0;
+    assert ecrecover(msgHashA, vA, rA, sA) != ecrecover(msgHashB, vB, rB, sB); 
+}
\ No newline at end of file

From 4f4b4f54803d77bcad930a4e5290e625841d2816 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Tue, 6 Feb 2024 15:06:50 +0200
Subject: [PATCH 2/9] Add readme and mutation for ecrecover example

---
 .../Ecrecover/ManualMutation/VerifyBug1.sol   | 70 ++++++++++++++++++
 .../Ecrecover/ManualMutation/VerifyBug2.sol   | 68 ++++++++++++++++++
 CVLByExample/Ecrecover/Readme.md              | 71 +++++++++++++++++++
 CVLByExample/Ecrecover/ecrecover.spec         | 29 +++++++-
 CVLByExample/Ecrecover/mutation.mconf         |  9 +++
 5 files changed, 245 insertions(+), 2 deletions(-)
 create mode 100644 CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol
 create mode 100644 CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol
 create mode 100644 CVLByExample/Ecrecover/Readme.md
 create mode 100644 CVLByExample/Ecrecover/mutation.mconf

diff --git a/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol b/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol
new file mode 100644
index 00000000..b0d7f96d
--- /dev/null
+++ b/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol
@@ -0,0 +1,70 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// game developer depoloys contract
+contract Verify {
+
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external  returns (bool) {
+        return ecrecover(msgHash, v, r, s) == _addr;
+    }
+
+
+mapping (address => uint256) private nonces; 
+
+function executeMyFunctionFromSignature(
+    uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) external {
+
+    bytes32 hash = getHash(owner, myParam, deadline);
+
+    
+    address signer = ecrecover(hash, v, r, s);
+    require(signer == owner, "MyFunction: invalid signature");
+    require(signer != address(0), "ECDSA: invalid signature");
+
+    require(block.timestamp < deadline, "MyFunction: signed transaction expired");
+    // nonces[owner]++; // forgeting to update the nonces will result in possible multiple execution 
+
+    _myFunction(owner, myParam);
+}
+
+function _myFunction(address owner, uint256 myParam) internal {
+
+}
+
+function getHash(
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) public returns(bytes32) {
+    bytes32 eip712DomainHash = keccak256(
+        abi.encode(
+            keccak256(
+                "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"
+            ),
+            keccak256(bytes("MyContractName")),
+            keccak256(bytes("1")),
+            address(this)
+        )
+    );
+
+    bytes32 hashStruct = keccak256(
+        abi.encode(
+            keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"),
+            owner,
+            myParam,
+            nonces[owner],
+            deadline
+        )
+    );
+
+    return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct));
+}
+
+
+}
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol b/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol
new file mode 100644
index 00000000..2e81e4cc
--- /dev/null
+++ b/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol
@@ -0,0 +1,68 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// game developer depoloys contract
+contract Verify {
+
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external  returns (bool) {
+        return ecrecover(msgHash, v, r, s) == _addr;
+    }
+
+
+mapping (address => uint256) private nonces; 
+
+function executeMyFunctionFromSignature(
+    uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) external {
+
+    bytes32 hash = getHash(/*owner*/ msg.sender, myParam, deadline); // computing the has on the wrong address
+
+    
+    address signer = ecrecover(hash, v, r, s);
+    require(signer == owner, "MyFunction: invalid signature");
+    require(signer != address(0), "ECDSA: invalid signature");
+
+    require(block.timestamp < deadline, "MyFunction: signed transaction expired");
+    nonces[owner]++; 
+
+    _myFunction(owner, myParam);
+}
+
+function _myFunction(address owner, uint256 myParam) internal {
+
+}
+
+function getHash(
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) public returns(bytes32) {
+    bytes32 eip712DomainHash = keccak256(
+        abi.encode(
+            keccak256(
+                "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"
+            ),
+            keccak256(bytes("MyContractName")),
+            keccak256(bytes("1")),
+            address(this)
+        )
+    );
+
+    bytes32 hashStruct = keccak256(
+        abi.encode(
+            keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"),
+            owner,
+            myParam,
+            nonces[owner],
+            deadline
+        )
+    );
+
+    return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct));
+}
+}
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md
new file mode 100644
index 00000000..fbf92077
--- /dev/null
+++ b/CVLByExample/Ecrecover/Readme.md
@@ -0,0 +1,71 @@
+# Ercecover Example
+
+## Overview
+This repository contains a smart contract named `Verify` that implements a signature verification mechanism using the `ecrecover` function. The contract includes a function `executeMyFunctionFromSignature` that allows a user to execute a specific function if the provided signature is valid. The example demonstrates new CVL feature which is cvl function version of the same ercecover function implemented in CVL.
+
+## Executions
+
+1. **Certora Run for ecrecover**
+    - Command:
+        ```bash
+        certoraRun ecrecover.conf --server production --prover_version master
+        ```
+    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/a86d458466c54009b8f3967bfbe6d168?anonymousKey=9939ccdd7e0e95cb77baca6b671f9ecd72e2b8b4)
+
+2. **Certora Mutate**
+    - Command:
+        ```bash
+        certoraMutate --mutation_conf mutation.mconf --prover_conf ecrecover.conf --server production
+        ```
+    - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=e58f1abb-146b-43bc-b06c-ba439a8491e3&anonymousKey=80175575-c70a-4fff-8b12-bcb8cf2fe904)
+
+The mutation execution contains 2 manual injection bugs locating under ManualMutation folder.
+
+## Smart Contract
+
+The smart contract, `Verify`, provides a method `isSigned` for signature verification and `executeMyFunctionFromSignature` for executing a function based on a valid signature. It also includes a method `getHash` for generating a hash used in the signature process.
+
+The contract follows the EIP-712 standard for domain separation and signature verification. The functions implement checks for signature uniqueness, zero value, determinism, and dependencies on `r` and `s`.
+
+## Certora Verification Language (CVL) Properties
+
+### ecrecover Properties
+
+1. **Zero Value**
+   - `ecrecover(0, v, r, s) == 0`
+
+2. **Deterministic**
+   - `ecrecover(msgHash, v, r, s) == _addr` on different calls
+
+3. **Uniqueness of Signature**
+   - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash', v, r, s) == 0` where `msgHash' != msgHash`
+
+4. **Dependency on r and s**
+   - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r', s) == 0` where `r' != r`
+   - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r, s') == 0` where `s' != s`
+
+### High-Level Properties
+
+1. **Single Verifier**
+   - A single address can verify a signature, and different addresses cannot verify the same signature.
+
+2. **Owner Signature Uniqueness**
+   - For a given address, two different messages cannot have the same valid signature.
+
+3. **Hash Uniqueness**
+   - Two different sets of parameters result in unique hash values.
+
+4. **Only Single User Can Execute**
+   - Only a single user, specified by the address, can successfully execute a function.
+
+5. **Signed Params and Deadline**
+   - The parameters and deadlines signed by the same address are the same.
+
+6. **Two Different Signatures**
+   - Two different messages signed by the same address have different signatures.
+
+7. **Signed Messages Executed Once**
+   - Once a message is executed, it cannot be executed again.
+
+
+For a comprehensive guide on Certora Verification Language, refer to [Certora Documentation](https://docs.certora.com).
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
index a9e0bd92..e1a791f6 100644
--- a/CVLByExample/Ecrecover/ecrecover.spec
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -185,12 +185,37 @@ rule signedParamAndDeadline(uint8 v,
 }
 
 
-
+/***
+ A signer can sign two different messages, in this case they have different signature 
+**/
 rule twoDifferent() {
     ecrecoverAxioms();
     bytes32 msgHashA;  uint8 vA; bytes32 rA; bytes32 sA; 
     bytes32 msgHashB;  uint8 vB; bytes32 rB; bytes32 sB;
     require  msgHashA != msgHashB;
     require ecrecover(msgHashA, vA, rA, sA) != 0 && ecrecover(msgHashB, vB, rB, sB) != 0;
-    assert ecrecover(msgHashA, vA, rA, sA) != ecrecover(msgHashB, vB, rB, sB); 
+    satisfy ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB); 
+    assert ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB) =>
+                    (rA != rB || sA != sB || vA != vB );
+}
+
+/**
+Once a message is executed, it can not be executed again 
+**/
+rule signedMessagesExecutedOnce(uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address signer,
+    uint256 myParam,
+    uint256 deadline) {
+
+    env e1;
+    env e2;
+    ecrecoverAxioms();
+    //execute and assume succeeded
+    executeMyFunctionFromSignature(e1, v, r, s, signer, myParam, deadline);
+    //attemp to execute again, on a possible different env
+    executeMyFunctionFromSignature@withrevert(e2, v, r, s, signer, myParam, deadline);
+    bool reverted = lastReverted;
+    assert reverted ; 
 }
\ No newline at end of file
diff --git a/CVLByExample/Ecrecover/mutation.mconf b/CVLByExample/Ecrecover/mutation.mconf
new file mode 100644
index 00000000..b4a0c5b0
--- /dev/null
+++ b/CVLByExample/Ecrecover/mutation.mconf
@@ -0,0 +1,9 @@
+{ 
+  "gambit": {
+    "filename" : "Verify.sol",
+    "num_mutants": 5
+  },
+  "manual_mutants": {
+     "Verify.sol": "ManualMutation"
+  }
+}
\ No newline at end of file

From 36bc12d0bea39a2fa22208d7cbb880bcaf1fe838 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Tue, 6 Feb 2024 15:30:11 +0200
Subject: [PATCH 3/9] add cvl index for ecrecover

---
 CVLByExample/README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CVLByExample/README.md b/CVLByExample/README.md
index edbcf4e1..b549646b 100644
--- a/CVLByExample/README.md
+++ b/CVLByExample/README.md
@@ -37,6 +37,8 @@
 | **using**         | [`using`](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_link.spec#L14) |
 | **withrevert**    | [`withrevert`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L44) |
 | **CVL Type**  | [mathint](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L23), [method](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L83), [env](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L20) |
+| **ercecover**  | [example](https://github.com/Certora/Examples/blob/niv/Add-ecrecover-example/CVLByExample/Ecrecover/ecrecover.spec#L67) |
+
 
 
 These examples can serve as an introduction to CVL ( Certora Verification Language ).

From a0a3bfd2acaf97baa4de7e9b45370a80976785be Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Thu, 8 Feb 2024 14:36:31 +0200
Subject: [PATCH 4/9] add satsify to catch vacous changes

---
 CVLByExample/Ecrecover/Readme.md      | 4 ++--
 CVLByExample/Ecrecover/ecrecover.spec | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md
index fbf92077..22807023 100644
--- a/CVLByExample/Ecrecover/Readme.md
+++ b/CVLByExample/Ecrecover/Readme.md
@@ -10,14 +10,14 @@ This repository contains a smart contract named `Verify` that implements a signa
         ```bash
         certoraRun ecrecover.conf --server production --prover_version master
         ```
-    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/a86d458466c54009b8f3967bfbe6d168?anonymousKey=9939ccdd7e0e95cb77baca6b671f9ecd72e2b8b4)
+    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/a218d8e1d23f4fac8448986e1ab6b791?anonymousKey=6ab622105d88de9dd59b16bc31dfec9c9ab6e412)
 
 2. **Certora Mutate**
     - Command:
         ```bash
         certoraMutate --mutation_conf mutation.mconf --prover_conf ecrecover.conf --server production
         ```
-    - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=e58f1abb-146b-43bc-b06c-ba439a8491e3&anonymousKey=80175575-c70a-4fff-8b12-bcb8cf2fe904)
+    - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=ce01eaf2-addb-4337-967b-8596a9c7f3a0&anonymousKey=04f60762-34e4-4604-aea7-13aeec78c488)
 
 The mutation execution contains 2 manual injection bugs locating under ManualMutation folder.
 
diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
index e1a791f6..e6271c6d 100644
--- a/CVLByExample/Ecrecover/ecrecover.spec
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -149,6 +149,7 @@ rule onlySingleUserCanExecute(uint8 v,
     storage init = lastStorage; 
     //execute and assume succeeded
     executeMyFunctionFromSignature(e1, v, r, s, alice, myParam, deadline);
+    satisfy true;
     // compare another execution on the same state, look at reverting paths
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, bob, myParam, deadline) at init;
     bool success = !lastReverted;
@@ -177,6 +178,7 @@ rule signedParamAndDeadline(uint8 v,
     storage init = lastStorage; 
     //execute and assume succeeded
     executeMyFunctionFromSignature(e1, v, r, s, owner, myParamA, deadlineA);
+    satisfy true;
     // compare another execution on the same state, look at reverting paths
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, owner, myParamB, deadlineB) at init;
     bool success = !lastReverted;
@@ -214,6 +216,7 @@ rule signedMessagesExecutedOnce(uint8 v,
     ecrecoverAxioms();
     //execute and assume succeeded
     executeMyFunctionFromSignature(e1, v, r, s, signer, myParam, deadline);
+    satisfy true;
     //attemp to execute again, on a possible different env
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, signer, myParam, deadline);
     bool reverted = lastReverted;

From e13bb4c0b239d57c2d690e1b1af4eeab324120eb Mon Sep 17 00:00:00 2001
From: liav-certora <114004726+liav-certora@users.noreply.github.com>
Date: Sun, 11 Feb 2024 23:11:38 +0200
Subject: [PATCH 5/9] Add examples of usage of cli flags (#54)

* First index

* Update README.md
---
 CLIFlags/README.md                | 33 +++++++++++++++++++++++++++++++
 CLIFlags/link.conf                | 15 ++++++++++++++
 CLIFlags/loop_iter.conf           | 11 +++++++++++
 CLIFlags/method.conf              | 10 ++++++++++
 CLIFlags/msg.conf                 | 10 ++++++++++
 CLIFlags/multi_assert_check.conf  | 11 +++++++++++
 CLIFlags/optimistic_loop.conf     | 10 ++++++++++
 CLIFlags/parametric_contract.conf | 15 ++++++++++++++
 CLIFlags/rule.conf                | 12 +++++++++++
 CLIFlags/rule_sanity.conf         | 11 +++++++++++
 CLIFlags/solc.conf                | 11 +++++++++++
 CLIFlags/solc_evm_version.conf    | 11 +++++++++++
 CLIFlags/solc_via_ir.conf         | 10 ++++++++++
 CLIFlags/verify.conf              |  9 +++++++++
 14 files changed, 179 insertions(+)
 create mode 100644 CLIFlags/README.md
 create mode 100644 CLIFlags/link.conf
 create mode 100644 CLIFlags/loop_iter.conf
 create mode 100644 CLIFlags/method.conf
 create mode 100644 CLIFlags/msg.conf
 create mode 100644 CLIFlags/multi_assert_check.conf
 create mode 100644 CLIFlags/optimistic_loop.conf
 create mode 100644 CLIFlags/parametric_contract.conf
 create mode 100644 CLIFlags/rule.conf
 create mode 100644 CLIFlags/rule_sanity.conf
 create mode 100644 CLIFlags/solc.conf
 create mode 100644 CLIFlags/solc_evm_version.conf
 create mode 100644 CLIFlags/solc_via_ir.conf
 create mode 100644 CLIFlags/verify.conf

diff --git a/CLIFlags/README.md b/CLIFlags/README.md
new file mode 100644
index 00000000..fbd1bf01
--- /dev/null
+++ b/CLIFlags/README.md
@@ -0,0 +1,33 @@
+# Examples of CLI Flags for certoraRun
+
+This is an index of some of the CLI flags available in the certoraRun command along with some examples of runs. Each flag links to its corresponding documentation over at Certora Docs. In this folder you can also see some confs called `<flag>.conf` with examples of these flags on some of the other examples available in this repository.
+
+For more information about available CLI options go to: https://docs.certora.com/en/latest/docs/prover/cli/options.html
+
+| Flag | Examples |
+| ---- | -------- |
+| [--verify](https://docs.certora.com/en/latest/docs/prover/cli/options.html#verify) | Every run uses verify ([e.g.](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014)). |
+| [--msg](https://docs.certora.com/en/latest/docs/prover/cli/options.html#msg-description) | [Run with a message.](https://prover.certora.com/output/15800/1aa5389f01604c33817e4f9ccf2f70fc?anonymousKey=e6f6fbe19097097df6851846847f5139b930b394) |
+| [--rule](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-rule-name) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) /  [Selecting only 1 rule.](https://prover.certora.com/output/15800/c554c7baf7534fe0940c98c60883bc6f?anonymousKey=1cef55a4c343c50c82b40d7c400ae185ede867d8) |
+| [--method](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#method-method-signature) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) / [Only 1 method used.](https://prover.certora.com/output/15800/3cf9410d78014c2f91835a5f8aa60767?anonymousKey=8392f2471d7507a21fd990a19ad0611592261f1e) |
+| [--parametric_contracts](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#parametric-contracts-contract-name) | [A LiquidityPool run without specifying.](https://prover.certora.com/output/15800/7ba2e8562afd4a5782f282059a0c1f00?anonymousKey=e12b94385957f1ebb14c0c1d8a77ec6f8765da7a) / [With specifying a contract.](https://prover.certora.com/output/15800/309c9ba5749e41b6b5a8b151ab3dd616?anonymousKey=44524f6189d23054e528c2a3ba97cc21112194fd) |
+| [--multi_assert_check](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#multi-assert-check) | [false](https://prover.certora.com/output/15800/e11354b5e03441cc9ac1d210fe686347?anonymousKey=911ba098228465f7c6fc0ba1d4d40cbde83bef94) / [true](https://prover.certora.com/output/15800/23c97944b0074bebb7e79ad4cd852984?anonymousKey=6e4c43f376883162646e5c61101abdcf36131c4e) |
+| [--independent_satisfy](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#independent-satisfy) | |
+| [--rule_sanity](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-sanity) | [none](https://prover.certora.com/output/15800/16fdf7aa282243e591889d9ec27a71ef?anonymousKey=6bdd16c5780e0127246ddc3eea3ee8a22c9729b8) / [basic](https://prover.certora.com/output/15800/2c5aa93c4bc54a939dea395202c0e47c?anonymousKey=bf07b5bdc3a7c7b28fda762942b02456731d2371) / [advanced](https://prover.certora.com/output/15800/e44ef408e1794a8fa32178f63fbe83da?anonymousKey=4afd4e7f98fc3d11d03b0a8522d417a2671f70fe) |
+| [--solc](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc) | [ERC20 compiled with solc8.0](https://prover.certora.com/output/15800/aa8e3c59b7434058a1f0927f6cd1da77?anonymousKey=099deb423f4cb86913f8a536309ea8a64511ca46) / [compiled with solc8.10](https://prover.certora.com/output/15800/c67c4072730d40f7b081556ddf78334e?anonymousKey=e9d7ffddc9f338e3a865505fbbe18f095823ae43) |
+| [--solc_map](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-map) | |
+| [--solc_optimize](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-optimize) | |
+| [--solc_via_ir](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-via-ir) | [false](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014) / [true](https://prover.certora.com/output/15800/4a29b3f21b884b8d8fc5550f61fa45b7?anonymousKey=f1909b5b181ae4534377501a3c06c896bfff2d67) |
+| [--solc_evm_version](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-evm-version) | [ERC20 with Berlin](https://prover.certora.com/output/15800/1d55dc0613b444f2a690fce8f645d9d1?anonymousKey=9efa9f0b59bfc8c37aa7c9d0d8573c9d99f1c2cf) / [ERC20 with London](https://prover.certora.com/output/15800/115e1f215f344fefb7dd389cb4db9d9f?anonymousKey=75c515fd97ff0ae21b887b5915db180d807dc9d2) |
+| [--solc_allow_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-allow-path) | Every conf example in this folder has it. |
+| [--packages_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages-path) | |
+| [--packages](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages) | |
+| [--optimistic_loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-loop) | [false](https://prover.certora.com/output/15800/8db8b5eaeb244ba490394e05edac0fe1?anonymousKey=5067d0c0908cc2f1cb348e8b163bfec327884cee) / [true](https://prover.certora.com/output/15800/89e59b62f44f439c9502363cef4e7b49?anonymousKey=bac549ca44168b6e0b282a980240c247b34d77ee) |
+| [--loop_iter](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#loop-iter) | [A run with 1 loop unrolling](https://prover.certora.com/output/15800/9b085d85bcc345d5bd2612f8bea5da98?anonymousKey=a6c544d73525dcb582eba2b971d85d97c16b35db) / [Same run with 3 loop unrolling](https://prover.certora.com/output/15800/0b152fe8cfcc41168429a287fa2ba7f8?anonymousKey=38fd94f0ac9bd36f3cecb23d8275b23b864e2d77) |
+| [--optimistic_summary_recursion](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-summary-recursion) | |
+| [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | |
+| [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | |
+| [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | |
+| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad) |
+| [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | |
+| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | |
\ No newline at end of file
diff --git a/CLIFlags/link.conf b/CLIFlags/link.conf
new file mode 100644
index 00000000..c82e46f9
--- /dev/null
+++ b/CLIFlags/link.conf
@@ -0,0 +1,15 @@
+{
+    "files": [
+        "../DEFI/LiquidityPool/contracts/Pool.sol",
+        "../DEFI/LiquidityPool/contracts/Asset.sol",
+        "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
+    ],
+    "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
+    // Link a field in the contract to another contract.
+    "link": [
+        "Pool:asset=Asset"
+    ],
+    
+    "parametric_contracts": ["Pool"],
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/loop_iter.conf b/CLIFlags/loop_iter.conf
new file mode 100644
index 00000000..283210fc
--- /dev/null
+++ b/CLIFlags/loop_iter.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/NativeBalances/contracts/Auction.sol",
+    ],
+    "verify": "Auction:../CVLByExample/NativeBalances/certora/specs/Auction.spec",
+    // Set number of loop unrolling for loops.
+    "loop_iter": "3",
+
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/method.conf b/CLIFlags/method.conf
new file mode 100644
index 00000000..8701c6cd
--- /dev/null
+++ b/CLIFlags/method.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Use only specific method for parametric rules and invariants.
+    "method": "transfer(address,uint256)",
+    
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/msg.conf b/CLIFlags/msg.conf
new file mode 100644
index 00000000..3f60816c
--- /dev/null
+++ b/CLIFlags/msg.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+    // Add a message.
+    "msg": "This run will have a message :)",
+
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/multi_assert_check.conf b/CLIFlags/multi_assert_check.conf
new file mode 100644
index 00000000..3924defd
--- /dev/null
+++ b/CLIFlags/multi_assert_check.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/Optional/contracts/Base.sol",
+        "../CVLByExample/Optional/contracts/Base.sol:Partial",
+    ],
+    "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
+    // Enable multi asserts.
+    "multi_assert_check": true,
+
+    "solc_allow_path": "../"
+}
diff --git a/CLIFlags/optimistic_loop.conf b/CLIFlags/optimistic_loop.conf
new file mode 100644
index 00000000..1b73c9f2
--- /dev/null
+++ b/CLIFlags/optimistic_loop.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Consider only paths in which the loop unwind condition holds.
+    "optimistic_loop": true,
+    
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/parametric_contract.conf b/CLIFlags/parametric_contract.conf
new file mode 100644
index 00000000..47adf846
--- /dev/null
+++ b/CLIFlags/parametric_contract.conf
@@ -0,0 +1,15 @@
+{
+    "files": [
+        "../DEFI/LiquidityPool/contracts/Pool.sol",
+        "../DEFI/LiquidityPool/contracts/Asset.sol",
+        "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
+    ],
+    "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
+    // Specify on which contracts to run parametric rules.
+    "parametric_contracts": ["Pool"],
+
+    "link": [
+        "Pool:asset=Asset"
+    ],
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/rule.conf b/CLIFlags/rule.conf
new file mode 100644
index 00000000..76a33598
--- /dev/null
+++ b/CLIFlags/rule.conf
@@ -0,0 +1,12 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Select only a specific rule.
+    "rule": [
+        "mintIntegrity"
+    ],
+    
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/rule_sanity.conf b/CLIFlags/rule_sanity.conf
new file mode 100644
index 00000000..b3ea3dc9
--- /dev/null
+++ b/CLIFlags/rule_sanity.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/Optional/contracts/Base.sol",
+        "../CVLByExample/Optional/contracts/Base.sol:Partial",
+    ],
+    "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
+    // Perform sanity check, set to none/basic/advanced.
+    "rule_sanity": "advanced",
+
+    "solc_allow_path": "../"
+}
diff --git a/CLIFlags/solc.conf b/CLIFlags/solc.conf
new file mode 100644
index 00000000..c863aead
--- /dev/null
+++ b/CLIFlags/solc.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Set the Solidity compiler version used.
+    "solc": "solc8.10",
+    
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/solc_evm_version.conf b/CLIFlags/solc_evm_version.conf
new file mode 100644
index 00000000..b7be2d65
--- /dev/null
+++ b/CLIFlags/solc_evm_version.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Set the EVM version used.
+    "solc_evm_version": "london",
+    
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/solc_via_ir.conf b/CLIFlags/solc_via_ir.conf
new file mode 100644
index 00000000..ad68801d
--- /dev/null
+++ b/CLIFlags/solc_via_ir.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+    // Enable IR based code generator.
+    "solc_via_ir": true,
+
+    "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CLIFlags/verify.conf b/CLIFlags/verify.conf
new file mode 100644
index 00000000..b4d2f720
--- /dev/null
+++ b/CLIFlags/verify.conf
@@ -0,0 +1,9 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    // Verify BallGame contract against the specified spec.
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+    
+    "solc_allow_path": "../"
+}
\ No newline at end of file

From 9faffb2aaa0386157bb0016c3dd4b00048e2098d Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Mon, 12 Feb 2024 13:54:47 +0200
Subject: [PATCH 6/9] add revert condition rule still need to fix direct
 storage bug

---
 CVLByExample/Ecrecover/Readme.md      |  2 +-
 CVLByExample/Ecrecover/ecrecover.spec | 64 ++++++++++++++++++++++++---
 2 files changed, 60 insertions(+), 6 deletions(-)

diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md
index 22807023..90db86b4 100644
--- a/CVLByExample/Ecrecover/Readme.md
+++ b/CVLByExample/Ecrecover/Readme.md
@@ -10,7 +10,7 @@ This repository contains a smart contract named `Verify` that implements a signa
         ```bash
         certoraRun ecrecover.conf --server production --prover_version master
         ```
-    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/a218d8e1d23f4fac8448986e1ab6b791?anonymousKey=6ab622105d88de9dd59b16bc31dfec9c9ab6e412)
+    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/259bb33a779b420aa6978aece0e506f0?anonymousKey=a666d86ce2aaeee393274d24259fd08af5a38e86)
 
 2. **Certora Mutate**
     - Command:
diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
index e6271c6d..242a6ef8 100644
--- a/CVLByExample/Ecrecover/ecrecover.spec
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -148,16 +148,37 @@ rule onlySingleUserCanExecute(uint8 v,
     //save the current state
     storage init = lastStorage; 
     //execute and assume succeeded
+    address temp = ecrecover(getHash(bob, myParam, deadline), v, r, s);
     executeMyFunctionFromSignature(e1, v, r, s, alice, myParam, deadline);
-    satisfy true;
     // compare another execution on the same state, look at reverting paths
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, bob, myParam, deadline) at init;
     bool success = !lastReverted;
     //if it succeeded it must be the same owner, or an unrealistic hash collision
-    assert success => alice==bob ; 
+    assert success => ( alice==bob ) ; 
 }
 
 
+/*** 
+   # High level property : there is only single owner that can be used
+    A rule which proves that for a given set of parameters only a single owner can execute .
+    This property is implemented as a relational property - it compares two different executions on the same state.
+*/
+rule ownerIsSigner(uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline) {
+
+    env e;
+    ecrecoverAxioms();
+    //execute and assume succeeded
+    address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s);
+    executeMyFunctionFromSignature(e, v, r, s, owner, myParam, deadline);
+
+    assert owner == signer;
+}
+
 /*** 
    # High level property : params and deadline are signed 
 make sure the param and deadline are part of the signature 
@@ -178,7 +199,6 @@ rule signedParamAndDeadline(uint8 v,
     storage init = lastStorage; 
     //execute and assume succeeded
     executeMyFunctionFromSignature(e1, v, r, s, owner, myParamA, deadlineA);
-    satisfy true;
     // compare another execution on the same state, look at reverting paths
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, owner, myParamB, deadlineB) at init;
     bool success = !lastReverted;
@@ -216,9 +236,43 @@ rule signedMessagesExecutedOnce(uint8 v,
     ecrecoverAxioms();
     //execute and assume succeeded
     executeMyFunctionFromSignature(e1, v, r, s, signer, myParam, deadline);
-    satisfy true;
     //attemp to execute again, on a possible different env
     executeMyFunctionFromSignature@withrevert(e2, v, r, s, signer, myParam, deadline);
     bool reverted = lastReverted;
     assert reverted ; 
-}
\ No newline at end of file
+}
+
+rule checkHash(
+    address bob,
+    uint256 myParam,
+    uint256 deadline) {
+
+    env e1;
+    ecrecoverAxioms();
+    //execute and assume succeeded
+    assert getHash(bob, myParam, deadline) == getHash(bob, myParam, deadline);
+}
+
+rule CheckRevertCondition(uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline) {
+
+    env e;
+    ecrecoverAxioms();
+
+    //execute and assume succeeded
+    address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s);
+    
+    bool msgValue = e.msg.value != 0;
+    bool signerIsZero = signer == 0;
+    bool signerDiffFromOwner =  signer != owner;
+    bool noncesOverflow = currentContract.nonces[owner] + 1 > max_uint256;
+    bool blockTimestampPassDeadline = e.block.timestamp >= deadline;
+
+    bool shouldRevert =  msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline ; 
+    executeMyFunctionFromSignature@withrevert(e, v, r, s, owner, myParam, deadline);
+    assert shouldRevert <=> lastReverted;
+}

From 17104ab51f0d1322aed3898af91aad66f880f6a7 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Mon, 12 Feb 2024 16:07:06 +0200
Subject: [PATCH 7/9] update the example

---
 CVLByExample/Ecrecover/Readme.md      | 4 ++--
 CVLByExample/Ecrecover/ecrecover.spec | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md
index 90db86b4..c44f248d 100644
--- a/CVLByExample/Ecrecover/Readme.md
+++ b/CVLByExample/Ecrecover/Readme.md
@@ -10,14 +10,14 @@ This repository contains a smart contract named `Verify` that implements a signa
         ```bash
         certoraRun ecrecover.conf --server production --prover_version master
         ```
-    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/259bb33a779b420aa6978aece0e506f0?anonymousKey=a666d86ce2aaeee393274d24259fd08af5a38e86)
+    - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/01ce19bfd3fa4a3b98e216bf2c085c24?anonymousKey=f85d1e9348a4e5f8293700660f90f41eb96aa83e)
 
 2. **Certora Mutate**
     - Command:
         ```bash
         certoraMutate --mutation_conf mutation.mconf --prover_conf ecrecover.conf --server production
         ```
-    - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=ce01eaf2-addb-4337-967b-8596a9c7f3a0&anonymousKey=04f60762-34e4-4604-aea7-13aeec78c488)
+    - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=71f2ffd2-80ea-47b5-b3b9-29cc73c91752&anonymousKey=d3f0379a-9a60-4b34-9edb-7210e763a91e)
 
 The mutation execution contains 2 manual injection bugs locating under ManualMutation folder.
 
diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
index 242a6ef8..60438b30 100644
--- a/CVLByExample/Ecrecover/ecrecover.spec
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -272,7 +272,7 @@ rule CheckRevertCondition(uint8 v,
     bool noncesOverflow = currentContract.nonces[owner] + 1 > max_uint256;
     bool blockTimestampPassDeadline = e.block.timestamp >= deadline;
 
-    bool shouldRevert =  msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline ; 
+    bool shouldRevert =  noncesOverflow || msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline ; 
     executeMyFunctionFromSignature@withrevert(e, v, r, s, owner, myParam, deadline);
     assert shouldRevert <=> lastReverted;
 }

From 7b317e514dd2978e769033d3f3db22369dd722d8 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Mon, 12 Feb 2024 18:40:07 +0200
Subject: [PATCH 8/9] update the comment

---
 CVLByExample/Ecrecover/ecrecover.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec
index 60438b30..6d75da2a 100644
--- a/CVLByExample/Ecrecover/ecrecover.spec
+++ b/CVLByExample/Ecrecover/ecrecover.spec
@@ -159,7 +159,7 @@ rule onlySingleUserCanExecute(uint8 v,
 
 
 /*** 
-   # High level property : there is only single owner that can be used
+   # High level property : Owner must be the signer of the hash
     A rule which proves that for a given set of parameters only a single owner can execute .
     This property is implemented as a relational property - it compares two different executions on the same state.
 */

From 53af1ec3c60664ed79598e8b8bdc12d7ad6173e8 Mon Sep 17 00:00:00 2001
From: Niv vaknin <122722245+nivcertora@users.noreply.github.com>
Date: Sun, 18 Feb 2024 14:15:23 +0200
Subject: [PATCH 9/9] fix naming (#58)

---
 CVLByExample/Ecrecover/{ecrecover.conf => Fullecrecover.conf} | 0
 CVLByExample/Ecrecover/Readme.md                              | 4 ++--
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename CVLByExample/Ecrecover/{ecrecover.conf => Fullecrecover.conf} (100%)

diff --git a/CVLByExample/Ecrecover/ecrecover.conf b/CVLByExample/Ecrecover/Fullecrecover.conf
similarity index 100%
rename from CVLByExample/Ecrecover/ecrecover.conf
rename to CVLByExample/Ecrecover/Fullecrecover.conf
diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md
index c44f248d..842861cd 100644
--- a/CVLByExample/Ecrecover/Readme.md
+++ b/CVLByExample/Ecrecover/Readme.md
@@ -8,14 +8,14 @@ This repository contains a smart contract named `Verify` that implements a signa
 1. **Certora Run for ecrecover**
     - Command:
         ```bash
-        certoraRun ecrecover.conf --server production --prover_version master
+        certoraRun Fullecrecover.conf --server production --prover_version master
         ```
     - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/01ce19bfd3fa4a3b98e216bf2c085c24?anonymousKey=f85d1e9348a4e5f8293700660f90f41eb96aa83e)
 
 2. **Certora Mutate**
     - Command:
         ```bash
-        certoraMutate --mutation_conf mutation.mconf --prover_conf ecrecover.conf --server production
+        certoraMutate --mutation_conf mutation.mconf --prover_conf Fullecrecover.conf --server production
         ```
     - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=71f2ffd2-80ea-47b5-b3b9-29cc73c91752&anonymousKey=d3f0379a-9a60-4b34-9edb-7210e763a91e)