From d88f7a8bb855df1956ea01821c1315f87dae2007 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20Cauderlier?= Date: Wed, 12 Feb 2020 15:58:30 +0100 Subject: [PATCH] [Doc] Add a README --- README.org | 129 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 README.org diff --git a/README.org b/README.org new file mode 100644 index 0000000..e575833 --- /dev/null +++ b/README.org @@ -0,0 +1,129 @@ +#+Title: The Albert intermediate language for the Tezos blockchain + +* Introduction + +Albert is a programming language with the following characteristics: + +- Albert programs are *smart contracts* that run on [[https://tezos.com][the Tezos blockchain]]. + +- Albert is a *compiled* language. The target language of Albert + compiler is [[https://michelson.nomadic-labs.com][Michelson]], Tezos' stack-based, typed, smart-contract + language. + +- Albert is an *intermediate* language; its purpose is to serve as + a compilation target for higher-level Tezos smart-contract languages + such as [[https://ligolang.org][Ligo]], [[https://smartpy.io][SmartPy]], [[https://archetype-lang.org/][Archetype]], etc. + +- Albert is *formally specified* in [[https://www.cl.cam.ac.uk/~pes20/ott/top2.html][the Ott semantic framework]]. + +- Albert compiler is written in [[https://coq.inria.fr][the Coq proof assistant]] and can hence + be the subject of *formal certification*. + +* Installation + +The recommended way to install Albert is using [[https://opam.ocaml.org/][opam]]. + +* Organisation of the source base + +- [[./LICENSE][LICENSE]] + + This project is free and open source software under the MIT License. + +- [[./Makefile][Makefile]] + + The main compilation targets for this project are =make compiler= to + build the Albert compiler, =make doc= to build the documentation, + =make test= to run the test suite, and =make full= to build + everything. + +- [[./README.org][README.org]]: this file + +- [[./albert.opam][albert.opam]]: meta-information for the Opam package manager + +- [[./ott/][ott/]] + + The Albert language specification is written in the Ott semantic + framework. We use the export facility of Ott to translate this + specification into Coq (for both meta-theoretic reasoning and the + compiler definition), LaTeX (for documentation), OCamllex (for + lexing), and Menhir (for parsing). The language is specified as a + collection of small fragments; the [[./ott/base.ott][ott/base.ott]] file specifies the + base fragment of the language on top of which almost all other files + in this directory are built. The two exceptions are [[./ott/header.ott][ott/header.ott]] + (a hack for embedding =Require= directives early enough in the Coq + backend) and [[./ott/latex.ott][ott/latex.ott]] (configuration of the LaTeX output). + +- [[./coq/][coq/]] + + The Albert compiler is defined in Coq. The main file is + [[./coq/michocomp.v][coq/michocomp.v]]. + + The file [[./coq/aux.v][coq/aux.v]] is a collection of auxiliary lemmas. + + The file [[./coq/compiler_correctness.v][coq/compiler_correctness.v]] states the type correctness of + the compiler: the compiler always produces well-typed Michelson + programs of the expected type. The proof is admitted. + + The files [[./coq/int64.v][coq/int64.v]] and [[./coq/tez.v][coq/tez.v]] have been borrowed from + Mi-Cho-Coq; they are used to define the data type of mutez amounts. + + The file [[./coq/label_lexico.v][coq/label_lexico.v]] defines the lexicographic ordering of + strings (used to represent Albert labels) and proves some basic + lemmas about this relation. + + The file [[./coq/lexico_sort.v][coq/lexico_sort.v]] defines sorted lists of labels and sorted + records. + + The file [[./coq/michocomp_tests.v][coq/michocomp_tests.v]] contains unit tests on the compiler. + + The file [[./coq/operations.v][coq/operations.v]] defines the Coq versions of the Albert + builtins operations. + + The file [[./coq/pretty_printers.v][coq/pretty_printers.v]] defines an Albert pretty-printer that + is used for error messages and to debug the lexer and parser. + + The files [[./coq/progress.v][coq/progress.v]] and [[./coq/subject_reduction.v][coq/subject_reduction.v]] are meta + theoretical proofs (in progress) about the Albert language. + + The file [[./coq/typer.v][coq/typer.v]] defines a type-checker for Albert. This + type-checker enriches the Albert ADT with typing information useful + to the compiler. + +- [[./extraction][extraction/]] + + To actually run the compiler and to bind it to the lexer and parser, + we use Coq extraction to OCaml. The extraction by itself is a + side-effect of type-checking the [[./extraction/extraction.v][extraction/extraction.v]] file and + the binding between the extracted compiler, the lexer, and the + parser is defined in [[./extraction/albert_comp.ml][extraction/albert_comp.ml]]. A few string + manipulation functions are defined in file [[./extraction/aux.ml][extraction/aux.ml]] whose + interface is defined in [[./extraction/aux.mli][extraction/aux.mli]]. + +- [[./doc][doc/]] + + The Org-mode file [[./doc/proposal.org][doc/proposal.org]] is the source of the Albert + documentation [[./doc/proposal_final.pdf][doc/proposal_final.pdf]]. + +- [[./emacs/][emacs/]] + + The file [[./emacs/albert-mode.el][emacs/albert-mode.el]] defines a major mode for the Emacs + text editor for viewing and editing Albert source files. This mode + features indentation and code coloring (aka. font-locking). + +- [[./examples/][examples/]] + + A collection of examples of Albert files (with extension =.alb=) + that also serves as a test suite. + +- [[./parser/][parser/]] + + The only source file in this directory is [[./parser/menhir_lib.mly][parser/menhir_lib.mly]]; a + collection of useful Menhir macros that are used in Ott Menhir + backend. + +* Further resources + +- [[https://github.com/Vertmo/stage2019-rapport][Basile Pesin's internship report]] + +- [[https://arxiv.org/abs/2001.02630][Albert, an intermediate smart-contract language for the Tezos + blockchain]]: Accepted at [[https://fc20.ifca.ai/wtsc/][the WTSC'2020 workshop]]. -- GitLab