Spec of `keccak256(_owner, _token, _amount)` ?

[nrryuya]

keccak serves as a wrapper around the Keccak256 in KRYPTO.

    syntax Int ::= keccak ( WordStack ) [function, smtlib(smt_keccak)]
 // ------------------------------------------------------------------
    rule keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) [concrete]

• gnosis getTransactionHash (actually don't verify hash function, just abstract it) https://github.com/runtimeverification/verified-smart-contracts/blob/master/gnosis/gnosis-spec.ini#L215

[ehildenb]

@nrryuya are you asking about what the correct implementation of keccak is?

When doing proofs, we actually don't execute this function, only when doing concrete execution. Instead, we hold it as an uninterpereted function symbol (which we instruct with smtlib(smt_keccak)), and add lemmas about it being "injective enough" if needed.

[nrryuya]

#keccak(CALLER_ID: 0: CALL_VALUE)

[nrryuya]

I tried adding this in verificaton.k (like casper and gnosis) but deposit-succ spec don't pass.

    syntax Int ::= symkeccak ( Int ) [function, smtlib(smt_symkeccak)]
 // -------------------------------------------------------------------
    rule keccak(WS) => symkeccak(#asWord(WS))  requires notBool #isConcrete(WS)

    rule 0 <=Int symkeccak(N) => true

    rule symkeccak(N) <Int pow256 => true