-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathconstants.v
41 lines (27 loc) · 974 Bytes
/
constants.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
(**
This file includes constants used by other modules, byte, evm word,
evm address, etc.
**)
Require Import bbv.Word.
Module Constants.
(* Byte *)
Definition EVMByteSize: nat := 8.
Definition EVMByte := word EVMByteSize.
(* Word *)
Definition BytesInEVMWord: nat := 32.
Definition EVMWordSize: nat := BytesInEVMWord*EVMByteSize.
Definition EVMWord:= word EVMWordSize.
(* Address *)
Definition ByteInEVMAddr : nat := 20.
Definition EVMAddrSize : nat := ByteInEVMAddr*EVMByteSize.
Definition EVMAddr := word EVMAddrSize.
(* Predefined constants *)
Definition BZero: EVMByte := natToWord EVMByteSize 0.
Definition BOne : EVMByte := natToWord EVMByteSize 1.
Definition WZero: EVMWord := natToWord EVMWordSize 0.
Definition WOne : EVMWord := natToWord EVMWordSize 1.
Definition AZero: EVMAddr := natToWord EVMAddrSize 0.
Definition AOne : EVMAddr := natToWord EVMAddrSize 1.
(* Maximum size of the stack *)
Definition StackSize := 1024.
End Constants.