Skip to content

Commit e158f9a

Browse files
committed
revm: update the revm version
1 parent 0b2920f commit e158f9a

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+59318
-37453
lines changed

CoqOfRust/revm/translations/interpreter/gas.v

Lines changed: 727 additions & 48 deletions
Large diffs are not rendered by default.

CoqOfRust/revm/translations/interpreter/gas/calc.v

Lines changed: 706 additions & 1390 deletions
Large diffs are not rendered by default.

CoqOfRust/revm/translations/interpreter/gas/constants.v

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Module gas.
1919
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 4 |))).
2020

2121
Definition value_RETF_GAS : Value.t :=
22-
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 4 |))).
22+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 3 |))).
2323

2424
Definition value_DATA_LOAD_GAS : Value.t :=
2525
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 4 |))).
@@ -78,7 +78,7 @@ Module gas.
7878
Definition value_CODEDEPOSIT : Value.t :=
7979
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 200 |))).
8080

81-
Definition value_INSTANBUL_SLOAD_GAS : Value.t :=
81+
Definition value_ISTANBUL_SLOAD_GAS : Value.t :=
8282
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 800 |))).
8383

8484
Definition value_SSTORE_SET : Value.t :=
@@ -132,5 +132,9 @@ Module gas.
132132

133133
Definition value_CALL_STIPEND : Value.t :=
134134
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 2300 |))).
135+
136+
Definition value_MIN_CALLEE_GAS : Value.t :=
137+
M.run
138+
ltac:(M.monadic (M.get_constant (| "revm_interpreter::gas::constants::CALL_STIPEND" |))).
135139
End constants.
136140
End gas.

CoqOfRust/revm/translations/interpreter/instruction_result.v

Lines changed: 2180 additions & 672 deletions
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)