All act specs are transformed into typed AST instances. The definition of this AST type can be found in Syntax/TimeAgnostic.hs.
The top level datatype here is a
Claim, and the output of the frontend states is a list of
Timed) claims. A
Claim is a sum type (enum) with four potential values:
S: typing information for storage variables
Act specs are intended to be fully exhaustive, for this reason we generate two claims from each constructor / behaviour in the spec:
Pass: The Pass claim states that if all preconditions in the iff block are true, then all executions will succeed, storage will be updated according to the storage block, and the specified return value will, in fact, be returned.
Fail: The Fail claim states that should any of the preconditions be false, all executions will revert.
Taken together a succesfull proof of these claims ensures that a given bytecode object implements only the behaviour specified in act and nothing else.
AST instances can be either
Timed (explicitly timed storage references) or
timed storage references), and this distinction is reflected at the type level (the
t parameter in
most of the data type definitions).
In some parts of an act spec (
ensures blocks), storage references must be qualified
with either the
post operator to disambiguate references to storage in the pre or post
state. In other blocks storage references are either implicitly refering to both pre and post states
invariants), or to the pre state only (e.g.
storage). In order to simplify implementation in
the various backends, there is a frontend stage (
annotate) that makes all implicit timings
explicit. The type parameter allows us to enforce the invariant that all backend stages always
Timed AST instances.
The act compilation pipeline is as follows:
flowchart LR; Source --> Lexer Lexer --> Parser; Parser --> Type[Type Checker]; Type --> Annotate; Annotate --> Enrich; Enrich --> SMT; Enrich --> Coq; Enrich --> Hevm; Enrich --> K;
The type checker takes an untyped AST, checks that none of the typing rules are violated, and produces a typed AST. The typechecker is defined in Type.hs and the core typed AST definition is in Syntax/TimeAgnostic.hs. The meaning of the timing parameter to the AST is described below in Timed vs Untimed AST instances.
The annotate stage makes any implicit timings explicit. This stage is implemented in Syntax/Annotated.hs.
The enrich stage adds preconditions to all behaviour / constructor / invariant instances based on the types of all variable references. This staged is implemented in Enrich.hs.
Stages that need to present errors to the user should return an instance of the
Error type defined
in Error.hs. This is a modified instance
of Data.Validation specialised to the act
context. This type allows us to accumulate multiple error messsages (useful if e.g. multiple syntax
errors are present), and we also have unified routines to pretty print these messages.