draft: implement eof_create_inputs definitions

[0xMushow]

No description provided.

[clarus]

We do not create any definitions in the links mode and only write run_new. This is one advantage of the links approach. Here the statement would be something like:

Definition run_new (caller : Address.t) (value : U256.t) (gas_limit : U64.t) (kind : EOFCreateKind.t) :
  {{
    (* the name is in the translation file and might be longer with more module prefixes *)
    Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInputs.new
      [] [] [φ caller; φ value; φ gas_limit; φ kind] ⇓
    fun (v : Self) => inl (φ v)
  }}.
Proof.

Then for an example of proof there is the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/revm/links/interpreter/interpreter/gas.v , although it is still quite experimental.

[clarus]

Same as with the new function!