generated-k-specification

requires "lemmas/ktoken-verification.k"

module MAX-SUCCESS-SPEC
  imports KTOKEN-VERIFICATION


  claim
  <kevm-specs>
    <kevm>
    <k> #runSymbTest => . </k>
    <exit-code> _ </exit-code>
    <mode> NORMAL </mode>
    <schedule> ISTANBUL </schedule>

    <ethereum>
      <evm>
        //<callStack> _ </callStack> //todo this version doesn't work: https://github.com/kframework/kore/issues/1677
        //<callStack> _:List </callStack> //Also doesn't work
        <callStack> .List </callStack> //This version works
        <interimStates> .List </interimStates> //Same limitations as for <callStack>
        <touchedAccounts> .Set => ?_ </touchedAccounts>

        <callState>
          <static> false </static> // NOTE: non-static call
          <callDepth> 0 => ?_ </callDepth>
          <callGas> #gas(_GAS) => ?_ </callGas>
          ( _ => ?_ )
        </callState>
        ( _ => ?_ )
      </evm>

      <network>
        <activeAccounts> SetItem(TESTER_ACCT) => ?_ </activeAccounts>
        <accounts>
          <account>
            <acctID>      TESTER_ACCT                         </acctID>
            <balance>     TESTER_ACCT_BALANCE                 </balance>
            <code>        #parseByteStack( "608060405234801561001057600080fd5b506004361061007d5760003560e01c8063a169625f1161005b578063a169625f146100da578063acf3b5291461013c578063e163183714610170578063fc171870146101b45761007d565b80634c63e56214610082578063663bc990146100b257806368226630146100bc575b600080fd5b6100b06004803
            <storage>     _ => ?_                             </storage>
            <origStorage> _ => ?_                             </origStorage>
            <nonce>       1 => ?_                             </nonce>
          </account>
          (.Bag => ?_)
        </accounts>
        ...
      </network>
    </ethereum>
    </kevm>

    <specStatus>      .SpecStatus => ?SPEC_STATUS       </specStatus>
    <specStatusTrace> .List       => ?SPEC_STATUS_TRACE </specStatusTrace>

    <testerAcctId> TESTER_ACCT </testerAcctId>
    <testName>     "test_1"  </testName>
  </kevm-specs>
     requires #rangeAddress(TESTER_ACCT) andBool notBool #isPrecompiledAccount(TESTER_ACCT, ISTANBUL)
      andBool #rangeUInt(256, TESTER_ACCT_BALANCE)
      ensures evalLTL((not assume-failed) implies (not assert-failed), ?SPEC_STATUS_TRACE) ==K true

endmodule