add partial ordering and reduce principal specs

certora/contracts/Starport.sol

@@ -214,7 +214,7 @@ contract Starport {
     }
 
     // Invoke without authorization checks used by external functions
-    function invokeNoticeInternal(bytes calldata notice, bytes32 noticeHash) internal returns (bytes memory) {
+    function invokeNoticeInternal(bytes calldata notice, bytes32 noticeHash) virtual internal returns (bytes memory) {
         if (isNoticeInvoked[noticeHash]) {
             emit NoticeReplay(noticeHash);
             return "";

certora/contracts/StarportHarness.sol

@@ -12,6 +12,8 @@ contract StarportHarness is Starport {
     bytes[] havocdNotices;
     bytes havocdNotice;
     bool public isAssert;
+
+    // for harness version of recover
     mapping(bytes32 => mapping(bytes => address)) recoverer;
 
     function noticeAlreadyInvoked() public returns (bool) {
@@ -36,14 +38,32 @@ contract StarportHarness is Starport {
 
     function invokeNoticeChain(bytes calldata theNotice, bytes[] calldata notices) public returns (bool) {
         if (isAssert) {
-            bytes32 noticeHash = this.hashNoticeExt(theNotice);
+            bytes32 noticeHash = hashNotice(theNotice);
             return isNoticeInvoked[noticeHash];
         } else {
             this.invokeChain(theNotice, notices);
             return true;
         }
     }
 
+    function partialOrderingCall(bytes calldata notice) public returns (uint256,uint256,bytes32) {
+        if (isAssert) {
+            bytes32 noticeHash = hashNotice(notice);
+            uint256 returnSize = invokeNoticeInternal(notice, noticeHash).length;
+            return (returnSize,0,0);
+        } else {
+            return myNoticeInfo(notice);
+        }
+    }
+
+    function myNoticeInfo(bytes calldata notice) public returns (uint256,uint256,bytes32) {
+        // copy-pasat from invokeNoticeInternal
+        (uint noticeEraId, uint noticeEraIndex, bytes32 noticeParent) =
+        abi.decode(notice[4:100], (uint, uint, bytes32));
+        bytes32 noticeHash = hashNotice(notice);
+        return (noticeEraId, noticeEraIndex, noticeHash);
+    }
+
     function noticeReturnsEmptyString() public returns (bool) {
         return this.invokeNoticeInternalExt(havocdNotice, this.hashNoticeExt(havocdNotice)).length == 0;
     }
@@ -104,12 +124,11 @@ contract StarportHarness is Starport {
     }
 
     function hashNoticeExt(bytes calldata theNotice) public returns (bytes32) {
-        require(theNotice.length < 32);
         return hashNotice(theNotice);
     }
 
     function hashNotice(bytes calldata data) override internal pure returns (bytes32) {
-        return keccak256(data);
+        return keccak256(data[4:68]);
     }
 
     function checkNoticeChain(bytes32 targetHash) public {

certora/contracts/StarportHarnessOrdering.sol

@@ -0,0 +1,52 @@
+pragma solidity ^0.8.1;
+pragma abicoder v2;
+
+import './StarportHarness.sol';
+
+
+contract StarportHarnessOrdering is StarportHarness {
+    constructor(ICash cash_, address admin_) StarportHarness(cash_, admin_) {}
+
+    function invokeNoticeInternal(bytes calldata notice, bytes32 noticeHash) override internal returns (bytes memory) {
+        if (isNoticeInvoked[noticeHash]) {
+            emit NoticeReplay(noticeHash);
+            return "";
+        }
+
+        isNoticeInvoked[noticeHash] = true;
+
+        require(notice.length >= 100, "Must have full header"); // 4 + 3 * 32
+        require(notice[0] == MAGIC_HEADER[0], "Invalid header[0]");
+        require(notice[1] == MAGIC_HEADER[1], "Invalid header[1]");
+        require(notice[2] == MAGIC_HEADER[2], "Invalid header[2]");
+        require(notice[3] == MAGIC_HEADER[3], "Invalid header[3]");
+
+        (uint noticeEraId, uint noticeEraIndex, bytes32 noticeParent) =
+            abi.decode(notice[4:100], (uint, uint, bytes32));
+
+        noticeParent; // unused
+
+        bool startNextEra = noticeEraId == eraId + 1 && noticeEraIndex == 0;
+
+        require(
+            noticeEraId <= eraId || startNextEra,
+            "Notice must use existing era or start next era"
+        );
+
+        if (startNextEra) {
+            eraId++;
+        }
+
+        // bytes memory calldata_ = bytes(notice[100:]);
+        // (bool success, bytes memory callResult) = address(this).call(calldata_);
+        // if (!success) {
+        //     require(false, _getRevertMsg(callResult));
+        // }
+
+        // emit NoticeInvoked(uint32(noticeEraId), uint32(noticeEraIndex), noticeHash, callResult);
+
+        // return callResult;
+
+        return "success";
+    }
+}

certora/readme.txt

@@ -1,8 +1,10 @@
+
  - Run Scripts
     CashToken:
      - runCashToken.sh: specs without any summarizing
      - runCashHarness.sh: spects summarizing index as 1e18 and axiomatizing
                           amountToPrincipal as monotonic
     Starport:
-     - runStarportHarness.sh: specs, no summaries but harnessing needed mostly because
-                              we have arrays as arguments
+     - runStarportHarness.sh: specs, no summaries but harnessing needed
+     - runStarportHarnessOrdering.sh:  partial ordering spec, override invokeNoticeInternal to not
+                                       perform the function call since this havocs all storage

certora/runStarportHarness.sh

@@ -4,5 +4,6 @@ certoraRun.py contracts/StarportHarness.sol \
 	spec/harnesses/ExcessiveERC20.sol \
 	contracts/CashToken.sol \
 	--verify StarportHarness:spec/Starport.spec \
-	--solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3  \
-	--staging --msg "Starport with Harness: ERC20 etc."
+	--solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3 \
+	--cache "the-starport-cache" \
+	--cloud --msg "Starport with Harness"

certora/runStarportHarnessOrdering.sh

@@ -0,0 +1,9 @@
+certoraRun.py contracts/StarportHarnessOrdering.sol \
+	spec/harnesses/ERC20.sol \
+	spec/harnesses/NonStandardERC20.sol \
+	spec/harnesses/ExcessiveERC20.sol \
+	contracts/CashToken.sol \
+	--verify StarportHarnessOrdering:spec/StarportOrdering.spec \
+	--solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3 \
+	--cache "starport-ordering" \
+	--cloud --msg "Starport with Harness: Notice Partial Ordering"

certora/spec/CashTokenHarness.spec

@@ -392,6 +392,33 @@ But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOthe
     assert newBalanceOfOther >= origBalanceOfOther;
 }
 
+/**
+ * @ERC20 modified
+ * @status	passing:	most
+ *			timeout:	burn
+ */
+senderCanOnlyReduceHerOwnPrincipal( method f, address sender, address other)
+description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's.
+But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther."
+{
+    env e;
+    require other != sender;
+	uint256 origBalanceOfOther = sinvoke cashPrincipal(other);
+
+    calldataarg arg;
+	env ef;
+	require ef.msg.sender == sender;
+	require f.selector != transferFrom(address,address,uint256).selector;
+	invoke f(ef, arg);
+
+	env e2;
+    require e2.block.number >= e.block.number;
+
+	uint256 newBalanceOfOther = sinvoke cashPrincipal(other);
+
+    assert newBalanceOfOther >= origBalanceOfOther;
+}
+
 /**
  * @ERC20
  * @status	passing:	most
@@ -421,6 +448,34 @@ But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOthe
     assert newBalanceOfOther >= origBalanceOfOther || origAllowance >= origBalanceOfOther-newBalanceOfOther;
 }
 
+/**
+ * @ERC20 modified
+ * @status	passing:	most
+ *			timeout:	burn
+ */
+senderCanOnlyReduceHerOwnPrincipalUnlessAllowanceAllowsIt( method f, address sender, address other)
+description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's.
+But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther."
+{
+    env e;
+    require other != sender;
+	uint256 origBalanceOfOther = sinvoke cashPrincipal(other);
+
+	uint256 origAllowance = amountToPrincipal(e, allowance(e, other, sender));
+
+    calldataarg arg;
+	env ef;
+	require ef.msg.sender == sender;
+	invoke f(ef, arg);
+
+	env e2;
+    require e2.block.number >= e.block.number;
+
+	uint256 newBalanceOfOther = sinvoke cashPrincipal(other);
+
+    assert newBalanceOfOther >= origBalanceOfOther || origAllowance >= origBalanceOfOther-newBalanceOfOther;
+}
+
 /**
  * @ERC20
  * @status	passing