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
42
43
|
; Yul Library
;
; Copyright (C) 2023 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "YUL")
(include-book "concrete-syntax")
(include-book "abstract-syntax")
(include-book "static-semantics")
(include-book "dynamic-semantics")
(include-book "static-soundness")
(include-book "errors")
(include-book "abstract-syntax-induction-schemas")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ language
:parents (yul)
:short "A formalization of the Yul language in ACL2."
:long
(xdoc::topstring
(xdoc::p
"This formalization covers a generic form of Yul
that supports the types of the EVM dialect.
The formalization consists of
a concrete syntax,
an abstract syntax,
a static semantics, and
a dynamic semantics.
We plan to make this formalization more generic,
and in particular to also support types in other Yul dialects."))
:order-subtopics (concrete-syntax
abstract-syntax
static-semantics
dynamic-semantics
static-soundness
errors))
|
