Draft: add mechanized translation to Coq

coq/ethereum/__init__.ast

@@ -0,0 +1,39 @@
+Module(
+    body=[
+        Expr(
+            value=Constant(value="\n### Introduction\n\nSeeing as internet connections have been vastly expanding across the\nworld, spreading information has become as cheap as ever. Bitcoin, for\nexample, has demonstrated the possibility of creating a decentralized,\ntrade system that is accessible around the world. Namecoin is another\nsystem that built off of Bitcoin's currency structure to create other\nsimple technological applications.\n\nEthereum's goal is to create a cryptographically secure system in which\nany and all types of transaction-based concepts can be built. It provides\nan exceptionally accessible and decentralized system to build software\nand execute transactions.\n\nThis package contains a reference implementation, written as simply as\npossible, to aid in defining the behavior of Ethereum clients.\n")),
+        Import(
+            names=[
+                alias(name='sys')]),
+        Assign(
+            targets=[
+                Name(id='__version__', ctx=Store())],
+            value=Constant(value='0.1.0')),
+        Assign(
+            targets=[
+                Name(id='EVM_RECURSION_LIMIT', ctx=Store())],
+            value=BinOp(
+                left=Constant(value=1024),
+                op=Mult(),
+                right=Constant(value=12))),
+        Expr(
+            value=Call(
+                func=Attribute(
+                    value=Name(id='sys', ctx=Load()),
+                    attr='setrecursionlimit',
+                    ctx=Load()),
+                args=[
+                    Call(
+                        func=Name(id='max', ctx=Load()),
+                        args=[
+                            Name(id='EVM_RECURSION_LIMIT', ctx=Load()),
+                            Call(
+                                func=Attribute(
+                                    value=Name(id='sys', ctx=Load()),
+                                    attr='getrecursionlimit',
+                                    ctx=Load()),
+                                args=[],
+                                keywords=[])],
+                        keywords=[])],
+                keywords=[]))],
+    type_ignores=[])

coq/ethereum/__init__.v

@@ -0,0 +1,20 @@
+(* Generated *)
+(*
+### Introduction
+
+Seeing as internet connections have been vastly expanding across the
+world, spreading information has become as cheap as ever. Bitcoin, for
+example, has demonstrated the possibility of creating a decentralized,
+trade system that is accessible around the world. Namecoin is another
+system that built off of Bitcoin's currency structure to create other
+simple technological applications.
+
+Ethereum's goal is to create a cryptographically secure system in which
+any and all types of transaction-based concepts can be built. It provides
+an exceptionally accessible and decentralized system to build software
+and execute transactions.
+
+This package contains a reference implementation, written as simply as
+possible, to aid in defining the behavior of Ethereum clients.
+*)
+

coq/ethereum/arrow_glacier/__init__.ast

@@ -0,0 +1,18 @@
+Module(
+    body=[
+        Expr(
+            value=Constant(value='\nThe Arrow Glacier fork delays the difficulty bomb. There are no other changes\nin this fork.\n')),
+        ImportFrom(
+            module='ethereum.fork_criteria',
+            names=[
+                alias(name='ByBlockNumber')],
+            level=0),
+        Assign(
+            targets=[
+                Name(id='FORK_CRITERIA', ctx=Store())],
+            value=Call(
+                func=Name(id='ByBlockNumber', ctx=Load()),
+                args=[
+                    Constant(value=13773000)],
+                keywords=[]))],
+    type_ignores=[])

coq/ethereum/arrow_glacier/__init__.v

@@ -0,0 +1,7 @@
+(* Generated *)
+(*
+The Arrow Glacier fork delays the difficulty bomb. There are no other changes
+in this fork.
+*)
+
+Require ethereum.fork_criteria.

coq/ethereum/arrow_glacier/blocks.ast

@@ -0,0 +1,230 @@
+Module(
+    body=[
+        Expr(
+            value=Constant(value='\nA `Block` is a single link in the chain that is Ethereum. Each `Block` contains\na `Header` and zero or more transactions. Each `Header` contains associated\nmetadata like the block number, parent block hash, and how much gas was\nconsumed by its transactions.\n\nTogether, these blocks form a cryptographically secure journal recording the\nhistory of all state transitions that have happened since the genesis of the\nchain.\n')),
+        ImportFrom(
+            module='dataclasses',
+            names=[
+                alias(name='dataclass')],
+            level=0),
+        ImportFrom(
+            module='typing',
+            names=[
+                alias(name='Tuple'),
+                alias(name='Union')],
+            level=0),
+        ImportFrom(
+            module='ethereum_types.bytes',
+            names=[
+                alias(name='Bytes'),
+                alias(name='Bytes8'),
+                alias(name='Bytes32')],
+            level=0),
+        ImportFrom(
+            module='ethereum_types.frozen',
+            names=[
+                alias(name='slotted_freezable')],
+            level=0),
+        ImportFrom(
+            module='ethereum_types.numeric',
+            names=[
+                alias(name='U256'),
+                alias(name='Uint')],
+            level=0),
+        ImportFrom(
+            module='crypto.hash',
+            names=[
+                alias(name='Hash32')],
+            level=2),
+        ImportFrom(
+            module='fork_types',
+            names=[
+                alias(name='Address'),
+                alias(name='Bloom'),
+                alias(name='Root')],
+            level=1),
+        ImportFrom(
+            module='transactions',
+            names=[
+                alias(name='LegacyTransaction')],
+            level=1),
+        ClassDef(
+            name='Header',
+            bases=[],
+            keywords=[],
+            body=[
+                Expr(
+                    value=Constant(value='\n    Header portion of a block on the chain.\n    ')),
+                AnnAssign(
+                    target=Name(id='parent_hash', ctx=Store()),
+                    annotation=Name(id='Hash32', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='ommers_hash', ctx=Store()),
+                    annotation=Name(id='Hash32', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='coinbase', ctx=Store()),
+                    annotation=Name(id='Address', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='state_root', ctx=Store()),
+                    annotation=Name(id='Root', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='transactions_root', ctx=Store()),
+                    annotation=Name(id='Root', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='receipt_root', ctx=Store()),
+                    annotation=Name(id='Root', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='bloom', ctx=Store()),
+                    annotation=Name(id='Bloom', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='difficulty', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='number', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='gas_limit', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='gas_used', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='timestamp', ctx=Store()),
+                    annotation=Name(id='U256', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='extra_data', ctx=Store()),
+                    annotation=Name(id='Bytes', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='mix_digest', ctx=Store()),
+                    annotation=Name(id='Bytes32', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='nonce', ctx=Store()),
+                    annotation=Name(id='Bytes8', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='base_fee_per_gas', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1)],
+            decorator_list=[
+                Name(id='slotted_freezable', ctx=Load()),
+                Name(id='dataclass', ctx=Load())]),
+        ClassDef(
+            name='Block',
+            bases=[],
+            keywords=[],
+            body=[
+                Expr(
+                    value=Constant(value='\n    A complete block.\n    ')),
+                AnnAssign(
+                    target=Name(id='header', ctx=Store()),
+                    annotation=Name(id='Header', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='transactions', ctx=Store()),
+                    annotation=Subscript(
+                        value=Name(id='Tuple', ctx=Load()),
+                        slice=Tuple(
+                            elts=[
+                                Subscript(
+                                    value=Name(id='Union', ctx=Load()),
+                                    slice=Tuple(
+                                        elts=[
+                                            Name(id='Bytes', ctx=Load()),
+                                            Name(id='LegacyTransaction', ctx=Load())],
+                                        ctx=Load()),
+                                    ctx=Load()),
+                                Constant(value=Ellipsis)],
+                            ctx=Load()),
+                        ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='ommers', ctx=Store()),
+                    annotation=Subscript(
+                        value=Name(id='Tuple', ctx=Load()),
+                        slice=Tuple(
+                            elts=[
+                                Name(id='Header', ctx=Load()),
+                                Constant(value=Ellipsis)],
+                            ctx=Load()),
+                        ctx=Load()),
+                    simple=1)],
+            decorator_list=[
+                Name(id='slotted_freezable', ctx=Load()),
+                Name(id='dataclass', ctx=Load())]),
+        ClassDef(
+            name='Log',
+            bases=[],
+            keywords=[],
+            body=[
+                Expr(
+                    value=Constant(value='\n    Data record produced during the execution of a transaction.\n    ')),
+                AnnAssign(
+                    target=Name(id='address', ctx=Store()),
+                    annotation=Name(id='Address', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='topics', ctx=Store()),
+                    annotation=Subscript(
+                        value=Name(id='Tuple', ctx=Load()),
+                        slice=Tuple(
+                            elts=[
+                                Name(id='Hash32', ctx=Load()),
+                                Constant(value=Ellipsis)],
+                            ctx=Load()),
+                        ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='data', ctx=Store()),
+                    annotation=Name(id='bytes', ctx=Load()),
+                    simple=1)],
+            decorator_list=[
+                Name(id='slotted_freezable', ctx=Load()),
+                Name(id='dataclass', ctx=Load())]),
+        ClassDef(
+            name='Receipt',
+            bases=[],
+            keywords=[],
+            body=[
+                Expr(
+                    value=Constant(value='\n    Result of a transaction.\n    ')),
+                AnnAssign(
+                    target=Name(id='succeeded', ctx=Store()),
+                    annotation=Name(id='bool', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='cumulative_gas_used', ctx=Store()),
+                    annotation=Name(id='Uint', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='bloom', ctx=Store()),
+                    annotation=Name(id='Bloom', ctx=Load()),
+                    simple=1),
+                AnnAssign(
+                    target=Name(id='logs', ctx=Store()),
+                    annotation=Subscript(
+                        value=Name(id='Tuple', ctx=Load()),
+                        slice=Tuple(
+                            elts=[
+                                Name(id='Log', ctx=Load()),
+                                Constant(value=Ellipsis)],
+                            ctx=Load()),
+                        ctx=Load()),
+                    simple=1)],
+            decorator_list=[
+                Name(id='slotted_freezable', ctx=Load()),
+                Name(id='dataclass', ctx=Load())])],
+    type_ignores=[])

coq/ethereum/arrow_glacier/blocks.v

@@ -0,0 +1,20 @@
+(* Generated *)
+(*
+A `Block` is a single link in the chain that is Ethereum. Each `Block` contains
+a `Header` and zero or more transactions. Each `Header` contains associated
+metadata like the block number, parent block hash, and how much gas was
+consumed by its transactions.
+
+Together, these blocks form a cryptographically secure journal recording the
+history of all state transitions that have happened since the genesis of the
+chain.
+*)
+
+Require dataclasses.
+Require typing.
+Require ethereum_types.bytes.
+Require ethereum_types.frozen.
+Require ethereum_types.numeric.
+Require ethereum.crypto.hash.
+Require ethereum.arrow_glacier.fork_types.
+Require ethereum.arrow_glacier.transactions.