Skip to content

Commit 80e9f5e

Browse files
clarusclarus
committed
revm: add missing specification crate
1 parent 59df8c2 commit 80e9f5e

File tree

9 files changed

+3639
-0
lines changed

9 files changed

+3639
-0
lines changed

‎.github/workflows/rust.yml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,13 @@ jobs:
120120
cargo coq-of-rust
121121
rsync -acv src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*'
122122
cd ..
123+
# specification
124+
cd specification
125+
cargo coq-of-rust
126+
touch src/lib.rs
127+
cargo coq-of-rust
128+
rsync -acv src/ ../../../../CoqOfRust/revm/translations/specification/ --include='*/' --include='*.v' --exclude='*'
129+
cd ..
123130
cd ../../..
124131
endGroup
125132
startGroup "Translate Move Sui"

‎CoqOfRust/revm/translations/specification/constants.v‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
(* Generated by coq-of-rust *)
2+
Require Import CoqOfRust.CoqOfRust.
3+
4+
Module constants.
5+
Definition value_STACK_LIMIT : Value.t :=
6+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 1024 |))).
7+
8+
Definition value_MAX_CODE_SIZE : Value.t :=
9+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 24576 |))).
10+
11+
Definition value_MAX_INITCODE_SIZE : Value.t :=
12+
M.run
13+
ltac:(M.monadic
14+
(M.alloc (|
15+
BinOp.Wrap.mul (|
16+
Value.Integer IntegerKind.Usize 2,
17+
M.read (| M.get_constant (| "revm_specification::constants::MAX_CODE_SIZE" |) |)
18+
|)
19+
|))).
20+
21+
Definition value_CALL_STACK_LIMIT : Value.t :=
22+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1024 |))).
23+
End constants.

‎CoqOfRust/revm/translations/specification/eip170.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(* Generated by coq-of-rust *)
2+
Require Import CoqOfRust.CoqOfRust.
3+
4+
Module eip170.
5+
Definition value_MAX_CODE_SIZE : Value.t :=
6+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 24576 |))).
7+
End eip170.

‎CoqOfRust/revm/translations/specification/eip2.v‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
(* Generated by coq-of-rust *)
2+
Require Import CoqOfRust.CoqOfRust.
3+
4+
Module eip2.
5+
Definition value_SECP256K1N_HALF : Value.t :=
6+
M.run
7+
ltac:(M.monadic
8+
(M.alloc (|
9+
M.call_closure (|
10+
M.get_associated_function (|
11+
Ty.apply
12+
(Ty.path "ruint::Uint")
13+
[ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
14+
[],
15+
"from_be_bytes",
16+
[]
17+
|),
18+
[
19+
Value.Array
20+
[
21+
Value.Integer IntegerKind.U8 127;
22+
Value.Integer IntegerKind.U8 255;
23+
Value.Integer IntegerKind.U8 255;
24+
Value.Integer IntegerKind.U8 255;
25+
Value.Integer IntegerKind.U8 255;
26+
Value.Integer IntegerKind.U8 255;
27+
Value.Integer IntegerKind.U8 255;
28+
Value.Integer IntegerKind.U8 255;
29+
Value.Integer IntegerKind.U8 255;
30+
Value.Integer IntegerKind.U8 255;
31+
Value.Integer IntegerKind.U8 255;
32+
Value.Integer IntegerKind.U8 255;
33+
Value.Integer IntegerKind.U8 255;
34+
Value.Integer IntegerKind.U8 255;
35+
Value.Integer IntegerKind.U8 255;
36+
Value.Integer IntegerKind.U8 255;
37+
Value.Integer IntegerKind.U8 93;
38+
Value.Integer IntegerKind.U8 87;
39+
Value.Integer IntegerKind.U8 110;
40+
Value.Integer IntegerKind.U8 115;
41+
Value.Integer IntegerKind.U8 87;
42+
Value.Integer IntegerKind.U8 164;
43+
Value.Integer IntegerKind.U8 80;
44+
Value.Integer IntegerKind.U8 29;
45+
Value.Integer IntegerKind.U8 223;
46+
Value.Integer IntegerKind.U8 233;
47+
Value.Integer IntegerKind.U8 47;
48+
Value.Integer IntegerKind.U8 70;
49+
Value.Integer IntegerKind.U8 104;
50+
Value.Integer IntegerKind.U8 27;
51+
Value.Integer IntegerKind.U8 32;
52+
Value.Integer IntegerKind.U8 160
53+
]
54+
]
55+
|)
56+
|))).
57+
End eip2.

‎CoqOfRust/revm/translations/specification/eip4844.v‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
(* Generated by coq-of-rust *)
2+
Require Import CoqOfRust.CoqOfRust.
3+
4+
Module eip4844.
5+
Definition value_GAS_PER_BLOB : Value.t :=
6+
M.run
7+
ltac:(M.monadic
8+
(M.alloc (|
9+
BinOp.Wrap.shl (| Value.Integer IntegerKind.U64 1, Value.Integer IntegerKind.I32 17 |)
10+
|))).
11+
12+
Definition value_TARGET_BLOB_NUMBER_PER_BLOCK : Value.t :=
13+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 3 |))).
14+
15+
Definition value_MAX_BLOB_NUMBER_PER_BLOCK : Value.t :=
16+
M.run
17+
ltac:(M.monadic
18+
(M.alloc (|
19+
BinOp.Wrap.mul (|
20+
Value.Integer IntegerKind.U64 2,
21+
M.read (|
22+
M.get_constant (| "revm_specification::eip4844::TARGET_BLOB_NUMBER_PER_BLOCK" |)
23+
|)
24+
|)
25+
|))).
26+
27+
Definition value_MAX_BLOB_GAS_PER_BLOCK : Value.t :=
28+
M.run
29+
ltac:(M.monadic
30+
(M.alloc (|
31+
BinOp.Wrap.mul (|
32+
M.read (|
33+
M.get_constant (| "revm_specification::eip4844::MAX_BLOB_NUMBER_PER_BLOCK" |)
34+
|),
35+
M.read (| M.get_constant (| "revm_specification::eip4844::GAS_PER_BLOB" |) |)
36+
|)
37+
|))).
38+
39+
Definition value_TARGET_BLOB_GAS_PER_BLOCK : Value.t :=
40+
M.run
41+
ltac:(M.monadic
42+
(M.alloc (|
43+
BinOp.Wrap.mul (|
44+
M.read (|
45+
M.get_constant (| "revm_specification::eip4844::TARGET_BLOB_NUMBER_PER_BLOCK" |)
46+
|),
47+
M.read (| M.get_constant (| "revm_specification::eip4844::GAS_PER_BLOB" |) |)
48+
|)
49+
|))).
50+
51+
Definition value_MIN_BLOB_GASPRICE : Value.t :=
52+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1 |))).
53+
54+
Definition value_BLOB_GASPRICE_UPDATE_FRACTION : Value.t :=
55+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 3338477 |))).
56+
57+
Definition value_VERSIONED_HASH_VERSION_KZG : Value.t :=
58+
M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U8 1 |))).
59+
End eip4844.

0 commit comments

Comments
 (0)