requires "abstract-semantics.k"
requires "verification.k"

module PROOF-SPEC
  imports ETHEREUM-SIMULATION
  imports ABSTRACT-SEMANTICS
  imports VERIFICATION

  // rmul
  rule
    <k> #execute => #execute </k>
    <exit-code> 1 </exit-code>
    <mode> NORMAL </mode>
    <schedule> BYZANTIUM </schedule>
    <analysis> .Map </analysis> // not part of evm

    <ethereum>
      <evm>
        <output> _ </output>
        <statusCode> _ </statusCode>
        <callStack> _ </callStack>
        <interimStates> _ </interimStates>
        <touchedAccounts> _ => _ </touchedAccounts>

        <callState>
          <program> #asMapOpCodes(#dasmOpCodes(#parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806367b870af14610046575b600080fd5b34801561005257600080fd5b5061008560048036038101908080359060200190929190803590602001909291908035906020019092919050505061009b565b6040518082815260200191505060405180910390f35b6000806002840614600081146100b3578491506100b7565b8291505b50600282046002840493505b83156100fa576100d5818487886100ff565b945060028406156100ef576100ec818487856100ff565b91505b6002840493506100c3565b610142565b60008282029050818382041415600084141516156101205761011f610147565b5b8481018181101561013457610133610147565b5b848104915050949350505050565b61014c565b600080fd5b5093925050505600a165627a7a7230582012a5165e693c1e46176e27b7a9bf9ad99b696d20d5012720c153b44af91d4a5f0029"), BYZANTIUM)) </program>
          <programBytes> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806367b870af14610046575b600080fd5b34801561005257600080fd5b5061008560048036038101908080359060200190929190803590602001909291908035906020019092919050505061009b565b6040518082815260200191505060405180910390f35b6000806002840614600081146100b3578491506100b7565b8291505b50600282046002840493505b83156100fa576100d5818487886100ff565b945060028406156100ef576100ec818487856100ff565b91505b6002840493506100c3565b610142565b60008282029050818382041415600084141516156101205761011f610147565b5b8481018181101561013457610133610147565b5b848104915050949350505050565b61014c565b600080fd5b5093925050505600a165627a7a7230582012a5165e693c1e46176e27b7a9bf9ad99b696d20d5012720c153b44af91d4a5f0029") </programBytes>

          <id> ACCT_ID </id> // contract owner
          <caller> CALLER_ID </caller> // who called this contract; in the begining, origin // msg.sender

          <callData> _ </callData>

          <callValue> 0 </callValue>
          <wordStack> X : Y : BASE : HALF : JUMPTO : WS => JUMPTO : (X *Int Y +Int HALF) /Int BASE : WS </wordStack>
          <localMem> .Map => _ </localMem>
          <pc> 255 => 321 </pc>
          <gas> G => G -Int 139 </gas>
          <memoryUsed> 0 => _ </memoryUsed>
          <previousGas> _ => _ </previousGas>

          <static> false </static> // NOTE: non-static call
          <callDepth> CALL_DEPTH </callDepth>
        </callState>

        <substate>
          <selfDestruct> _ </selfDestruct>
          <log> _ </log>
          <refund> _ </refund> // TODO: more detail
        </substate>

        <gasPrice> _ </gasPrice>
        <origin> ORIGIN_ID </origin> // who fires tx

        <previousHash> _ </previousHash>
        <ommersHash> _ </ommersHash>
        <coinbase> _ </coinbase>
        <stateRoot> _ </stateRoot>
        <transactionsRoot> _ </transactionsRoot>
        <receiptsRoot> _ </receiptsRoot>
        <logsBloom> _ </logsBloom>
        <difficulty> _ </difficulty>
        <number> _ </number>
        <gasLimit> _ </gasLimit>
        <gasUsed> _ </gasUsed>
        <timestamp> _ </timestamp>
        <extraData> _ </extraData>
        <mixHash> _ </mixHash>
        <blockNonce> _ </blockNonce>

        <ommerBlockHeaders> _ </ommerBlockHeaders>
        <blockhash> _ </blockhash>
      </evm>

      <network>
        <activeAccounts> SetItem(ACCT_ID) _:Set

        </activeAccounts>

        <accounts>
          <account>
            <acctID> ACCT_ID </acctID>
            <balance> _ </balance>
            <code> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806367b870af14610046575b600080fd5b34801561005257600080fd5b5061008560048036038101908080359060200190929190803590602001909291908035906020019092919050505061009b565b6040518082815260200191505060405180910390f35b6000806002840614600081146100b3578491506100b7565b8291505b50600282046002840493505b83156100fa576100d5818487886100ff565b945060028406156100ef576100ec818487856100ff565b91505b6002840493506100c3565b610142565b60008282029050818382041415600084141516156101205761011f610147565b5b8481018181101561013457610133610147565b5b848104915050949350505050565b61014c565b600080fd5b5093925050505600a165627a7a7230582012a5165e693c1e46176e27b7a9bf9ad99b696d20d5012720c153b44af91d4a5f0029") </code>
            <storage>
              _
            </storage>
            <nonce> _ </nonce>
          </account>

          ...
        </accounts>

        <txOrder> _ </txOrder>
        <txPending> _ </txPending>
        <messages> _ </messages>
      </network>
    </ethereum>
    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
     andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
     andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
     andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
     andBool #sizeWordStack(WS) <Int 250
andBool #sizeWordStack(WS) >=Int 0
andBool HALF ==Int BASE /Int 2
andBool 0 <=Int X andBool X <Int pow256
andBool 0 <=Int Y andBool Y <Int pow256
andBool 0 <=Int X *Int Y andBool X *Int Y <Int pow256
andBool 0 <=Int X *Int Y +Int HALF andBool X *Int Y +Int HALF <Int pow256
andBool 1 <=Int BASE andBool BASE <Int pow256
andBool G >=Int 1000000000



endmodule