Unverified Commit d88f7a8b authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[Doc] Add a README

parent 38705cac
Pipeline #132212066 passed with stage
in 8 minutes and 38 seconds
#+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
- 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
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
- [[./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
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
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
* 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]].
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment