Laurel

The Laurel Language

Table of Contents

  1. 1. Introduction
  2. 2. Types
  3. 3. Expressions and Statements
  4. 4. Procedures
  5. 5. Programs
  6. 6. Implementation
  7. 7. Differences between Laurel and Core

1. Introduction🔗

Laurel is an intermediate verification language designed to serve as a target for popular garbage-collected languages that include imperative features, such as Java, Python, and JavaScript, where those languages have been extended to include verification specific constructs. Laurel tries to include any features that are common to those three languages.

Laurel enables doing various forms of verification:

  • Testing

  • (WIP) Property-based testing

  • (WIP) Bounded symbolic execution

  • Unbounded symbolic execution

  • (WIP) Data-flow analysis

1.1. Shared language features🔗

Here are some Laurel language features that are shared between the source languages:

  • Statements such as loops and return statements

  • Mutation of variables, including in expressions

  • Reading and writing of fields of references

  • Object oriented concepts such as inheritance, type checking, up and down casting and dynamic dispatch

  • (WIP) Error handling via exceptions

  • (WIP) Procedures types and procedures as values

  • (WIP) Parametric polymorphism

Laurel does not distinguish between statements and expressions. Expression-like or statement-like constructs can occur in the same positions. Each statement-expression has a type, which for statement-like constructs might be void.

1.2. Verification features🔗

On top of the above features, Laurel adds features that are useful specifically for verification:

  • Assert and assume statements

  • Loop invariants

  • Pre and postconditions for procedures

  • Modifies and reads clauses for procedures

  • (WIP) Decreases clauses for procedures and loops

  • (WIP) Immutable fields and constructors that support assigning to them

  • (WIP) Constrained types

  • (WIP) Type invariants

  • Forall and exists expressions

  • (WIP) Old and fresh expressions

  • Unbounded integer and real types

  • To be designed constructs for supporting proof writing

1.3. Verification design choices🔗

A peculiar choice of Laurel is that it does not require imperative code to be encapsulated using a functional specification. A reason for this is that sometimes the imperative code is as readable as the functional specification. For example:

procedure increment(counter: Counter)
  // In Laurel, this ensures clause can be left out
  ensures counter.value == old(counter.value) + 1
{
  counter.value := counter.value + 1;
};

1.4. Internal constructors and properties🔗

Some constructors and properties in the Laurel AST are marked for internal usage and should not be needed by Laurel users. Having these internal properties and constructors allows us to define an incremental translation to Core which improves maintainability.

2. Types🔗

Laurel's type system includes primitive types, collection types, and user-defined types.

2.1. Primitive Types🔗

🔗inductive type
Strata.Laurel.HighType : Type
Strata.Laurel.HighType : Type

The type system for Laurel programs.

HighType covers primitive types (TVoid, TBool, TInt, TReal, TFloat64, TString), internal types used by the heap parameterization pass (THeap, TTypedField), collection types (TSet), user-defined types (UserDefined), generic applications (Applied), value types (Pure), and intersection types (Intersection).

Constructors

TVoid : HighType

The void type, used for statements that produce no value.

TBool : HighType

Boolean type.

TInt : HighType

Arbitrary-precision integer type.

TFloat64 : HighType

64-bit floating point type. Required for JavaScript (number), also used by Python (float) and Java (double).

TReal : HighType

Mathematical real type. Maps to Core's real type.

TString : HighType

String type for text data.

THeap : HighType

Internal type representing the heap. Introduced by the heap parameterization pass; not accessible via grammar.

TTypedField (valueType : AstNode HighType) : HighType

Internal type for a field constant with a known value type. Introduced by the heap parameterization pass; not accessible via grammar.

TSet (elementType : AstNode HighType) : HighType

Set type, e.g. Set int.

TMap (keyType valueType : AstNode HighType) : HighType

Map type.

UserDefined (name : Identifier) : HighType

A Identifier to a user-defined composite or constrained type by name.

Applied (base : AstNode HighType)
  (typeArguments : List (AstNode HighType)) : HighType

A generic type application, e.g. List<Int>.

Pure (base : AstNode HighType) : HighType

A pure (value) variant of a composite type that uses structural equality instead of reference equality.

Intersection (types : List (AstNode HighType)) : HighType

An intersection of types. Used for implicit intersection types, e.g. Scientist & Scandinavian.

TBv (size : Nat) : HighType

Bitvector type of a given width.

TCore (s : String) : HighType

Temporary construct meant to aid the migration of Python->Core to Python->Laurel. Type "passed through" from Core. Intended to allow translations to Laurel to refer directly to Core.

Unknown : HighType

Type used internally by the Laurel compilation pipeline. This type is used when a resolution error occurs, to continue compilation without producing superfluous errors Any type can be assigned to unknown and unknown can be assigned to any type. The unknown type can not be represented in Core so its occurence will abort compilation before evaluating Core

MultiValuedExpr (types : List (AstNode HighType)) : HighType

An internal-only type produced by computeExprType for multi-output procedure calls. Consumed by the resolution arity check and highEq. Should never appear in a serialized program.

2.2. User-Defined Types🔗

User-defined types come in two categories: composite types and constrained types.

Composite types have fields and procedures, and may extend other composite types. Fields declare whether they are mutable and specify their type.

🔗structure
Strata.Laurel.CompositeType : Type
Strata.Laurel.CompositeType : Type

A composite defines a type with fields and instance procedures.

Composite types may extend other composite types, forming a type hierarchy that affects the results of IsType and AsType operations.

Constructor

Strata.Laurel.CompositeType.mk

Fields

name : Identifier

The type name.

extending : List Identifier

Names of composite types this type extends. The type hierarchy affects IsType and AsType results.

fields : List Field

The fields of this type.

instanceProcedures : List Procedure

Instance procedures (methods) defined on this type.

🔗structure
Strata.Laurel.Field : Type
Strata.Laurel.Field : Type

A field in a composite type. Fields declare their name, mutability, and type. Mutability affects what permissions are needed to access the field.

Constructor

Strata.Laurel.Field.mk

Fields

name : Identifier

The field name.

isMutable : Bool

Whether the field is mutable. Mutable fields require write permission.

type : HighTypeMd

The field's type.

Constrained types are defined by a base type and a constraint over the values of the base type. Algebraic datatypes can be encoded using composite and constrained types.

🔗structure
Strata.Laurel.ConstrainedType : Type
Strata.Laurel.ConstrainedType : Type

A constrained (refinement) type defined by a base type and a predicate.

Algebraic datatypes can be encoded using composite and constrained types. For example, Option<T> can be defined as a constrained type over Dynamic with the constraint value is Some<T> || value is Unit.

Constructor

Strata.Laurel.ConstrainedType.mk

Fields

name : Identifier

The constrained type's name.

base : HighTypeMd

The base type being refined.

valueName : Identifier

The name bound to the value in the constraint expression.

constraint : StmtExprMd

The predicate that values of this type must satisfy.

witness : StmtExprMd

A witness value proving the type is inhabited.

🔗inductive type
Strata.Laurel.TypeDefinition : Type
Strata.Laurel.TypeDefinition : Type

A user-defined type, either a composite type, a constrained type, an algebraic datatype, or a type alias.

Algebriac datatypes can also be encoded uses composite and constrained types. Here are two examples:

Example 1: composite Some<T> { value: T } constrained Option<T> = value: Dynamic | value is Some<T> || value is Unit

Example 2: composite Cons<T> { head: T, tail: List<T> } constrained List<T> = value: Dynamic | value is Cons<T> || value is Unit

Constructors

Composite (ty : CompositeType) : TypeDefinition

A composite (class-like) type with fields and methods.

Constrained (ty : ConstrainedType) : TypeDefinition

A constrained (refinement) type with a base type and predicate.

Datatype (ty : DatatypeDefinition) : TypeDefinition

An algebriac datatype.

Alias (ty : TypeAlias) : TypeDefinition

A type alias (e.g. MyInt = int). Eliminated before Core translation.

3. Expressions and Statements🔗

Laurel uses a unified StmtExpr type that contains both expression-like and statement-like constructs. This avoids duplication of shared concepts such as conditionals and variable declarations.

3.1. Operations🔗

🔗inductive type
Strata.Laurel.Operation : Type
Strata.Laurel.Operation : Type

Primitive operations available in Laurel expressions.

Operations are grouped into boolean operations (Eq, Neq, And, Or, Not, Implies), arithmetic operations (Neg, Add, Sub, Mul, Div, Mod, DivT, ModT), and comparison operations (Lt, Leq, Gt, Geq).

Equality on composite types uses reference equality for impure types and structural equality for pure ones.

Constructors

Eq : Operation

Equality test. Uses reference equality for impure composite types, structural equality for pure ones.

Neq : Operation

Inequality test.

And : Operation

Logical conjunction (eager).

Or : Operation

Logical disjunction (eager).

Not : Operation

Logical negation.

Implies : Operation

Logical implication (short-circuit).

AndThen : Operation

Short-circuit logical conjunction. Only evaluates the second argument if the first is true.

OrElse : Operation

Short-circuit logical disjunction. Only evaluates the second argument if the first is false.

Neg : Operation

Arithmetic negation. Works on Int and Float64.

Add : Operation

Addition. Works on Int and Float64.

Sub : Operation

Subtraction. Works on Int and Float64.

Mul : Operation

Multiplication. Works on Int and Float64.

Div : Operation

Euclidean division. Works on Int and Float64.

Mod : Operation

Euclidean modulus. Works on Int and Float64.

DivT : Operation

Truncation division.

ModT : Operation

Truncation modulus.

Lt : Operation

Less than. Works on Int and Real.

Leq : Operation

Less than or equal. Works on Int and Real.

Gt : Operation

Greater than. Works on Int and Real.

Geq : Operation

Greater than or equal. Works on Int and Real.

StrConcat : Operation

String concatenation.

3.2. The StmtExpr Type🔗

🔗inductive type
Strata.Laurel.StmtExpr : Type
Strata.Laurel.StmtExpr : Type

The unified statement-expression type for Laurel programs.

StmtExpr contains both statement-like constructs (conditionals, loops, assignments, returns) and expression-like constructs (literals, identifiers, operations, calls). Using a single type avoids duplication of shared concepts such as conditionals and variable declarations.

Constructors

IfThenElse (cond thenBranch : AstNode StmtExpr)
  (elseBranch : Option (AstNode StmtExpr)) : StmtExpr

Conditional with a then-branch and optional else-branch.

Block (statements : List (AstNode StmtExpr))
  (label : Option String) : StmtExpr

A sequence of statements with an optional label for Exit.

While (cond : AstNode StmtExpr)
  (invariants : List (AstNode StmtExpr))
  (decreases : Option (AstNode StmtExpr))
  (body : AstNode StmtExpr) : StmtExpr

A while loop with a condition, invariants, optional termination measure, and body. Only allowed in impure contexts.

Exit (target : String) : StmtExpr

Exit a labelled block. Models break and continue statements.

Return (value : Option (AstNode StmtExpr)) : StmtExpr

Return from the enclosing procedure with an optional value.

LiteralInt (value : Int) : StmtExpr

An integer literal.

LiteralBool (value : Bool) : StmtExpr

A boolean literal.

LiteralString (value : String) : StmtExpr

A string literal.

LiteralDecimal (value : StrataDDM.Decimal) : StmtExpr

A decimal literal.

Var (var : Variable) : StmtExpr

A variable reference or declaration. When var is Variable.Local, this is a reference that evaluates to the variable's value. When var is Variable.Declare, this is a declaration without an initializer (used as a standalone statement in a block).

Assign (targets : List (AstNode Variable))
  (value : AstNode StmtExpr) : StmtExpr

Assignment to one or more targets. Multiple targets are only supported with identifier targets and a call as the RHS.

PureFieldUpdate (target : AstNode StmtExpr)
  (fieldName : Identifier) (newValue : AstNode StmtExpr) :
  StmtExpr

Update a field on a pure (value) type, producing a new value.

StaticCall (callee : Identifier)
  (arguments : List (AstNode StmtExpr)) : StmtExpr

Call a static procedure by name with the given arguments.

PrimitiveOp (operator : Operation)
  (arguments : List (AstNode StmtExpr))
  (skipProof : Bool := false) : StmtExpr

Apply a primitive operation to the given arguments. The skipProof property is used internally. It means that any precondition of the operator, such as division has, should be ignored.

New (ref : Identifier) : StmtExpr

Create new object (new).

This : StmtExpr

Reference to the current object (this/self).

ReferenceEquals (lhs rhs : AstNode StmtExpr) : StmtExpr

Reference equality test between two expressions.

AsType (target : AstNode StmtExpr)
  (targetType : AstNode HighType) : StmtExpr

Type cast: treat the target as the given type.

IsType (target : AstNode StmtExpr)
  (type : AstNode HighType) : StmtExpr

Type test: check whether the target is an instance of the given type.

InstanceCall (target : AstNode StmtExpr)
  (callee : Identifier)
  (arguments : List (AstNode StmtExpr)) : StmtExpr

Call an instance method on a target object.

Quantifier (mode : QuantifierMode) (param : Parameter)
  (trigger : Option (AstNode StmtExpr))
  (body : AstNode StmtExpr) : StmtExpr

Quantification (universal or existential) over a typed parameter with an optional trigger.

Assigned (name : AstNode StmtExpr) : StmtExpr

Check whether a variable has been assigned.

Old (value : AstNode StmtExpr) : StmtExpr

Refer to the pre-state value of an expression in a postcondition.

Fresh (value : AstNode StmtExpr) : StmtExpr

Check whether a reference is freshly allocated. May only target impure composite types.

Assert (condition : Condition) : StmtExpr

Assert a condition, generating a proof obligation.

Assume (condition : AstNode StmtExpr) : StmtExpr

Assume a condition, restricting the state space.

ProveBy (value proof : AstNode StmtExpr) : StmtExpr

Attach a proof hint to a value. The semantics are those of value, but proof helps discharge assertions in value.

ContractOf (type : ContractType)
  (function : AstNode StmtExpr) : StmtExpr

Extract the contract (reads, modifies, precondition, or postcondition) of a function.

Abstract : StmtExpr

Marker for abstract contracts. Makes the containing type abstract.

All : StmtExpr

Refers to all objects in the heap. Used in reads or modifies clauses.

Hole (deterministic : Bool := true)
  (type : Option (AstNode HighType) := none) : StmtExpr

A hole represents an unknown expression. This can be used to represent programs that are still under development, for example the program 3 + The defining property of a hole is that interaction with it and other code should not produce any errors. Besides representing partial user programs, holes can also be used to handle under development parts of compilers that target Laurel.

  • deterministic: if true, the hole represents a deterministic unknown (translated as an uninterpreted function); if false, a nondeterministic unknown (translated as a havoced variable). Nondeterministic holes are not allowed in functions.

  • type: this property is used internally by Laurel and can be left to its default value. Internal usage: inferred by the hole type inference pass; none means not yet inferred.

3.3. Metadata🔗

All AST nodes can carry metadata via the AstNode wrapper.

🔗structure
Strata.Laurel.AstNode (t : Type) : Type
Strata.Laurel.AstNode (t : Type) : Type

A wrapper that pairs a value with source-level metadata such as source locations and annotations. All Laurel AST nodes are wrapped in AstNode so that error messages and verification conditions can refer back to the original source.

Constructor

Strata.Laurel.AstNode.mk

Fields

val : t

The wrapped value.

source : Option Strata.FileRange

Source location for this AST node.

4. Procedures🔗

Procedures are the main unit of specification and verification in Laurel.

🔗structure
Strata.Laurel.Procedure : Type
Strata.Laurel.Procedure : Type

A procedure in Laurel. Procedures are the main unit of specification and verification. Unlike separate functions and methods, Laurel uses a single general concept that covers both.

Constructor

Strata.Laurel.Procedure.mk

Fields

name : Identifier

The procedure's name.

inputs : List Parameter

Input parameters with their types.

outputs : List Parameter

Output parameters with their types. Multiple outputs are supported.

preconditions : List Condition

The preconditions that callers must satisfy.

decreases : Option (AstNode StmtExpr)

Optional termination measure for recursive procedures.

isFunctional : Bool

If true, the body may only have functional constructs, so no destructive assignments or loops.

body : Body

The procedure body: transparent, opaque, or abstract.

invokeOn : Option (AstNode StmtExpr)

Optional trigger for auto-invocation. When present, the translator also emits an axiom whose body is the ensures clause universally quantified over the procedure's inputs, with this expression as the SMT trigger.

🔗structure
Strata.Laurel.Parameter : Type
Strata.Laurel.Parameter : Type

A typed parameter for a procedure.

Constructor

Strata.Laurel.Parameter.mk

Fields

name : Identifier

The parameter name.

type : AstNode HighType

The parameter type.

🔗inductive type
Strata.Laurel.Body : Type
Strata.Laurel.Body : Type

The body of a procedure. A body can be transparent (with a visible implementation), opaque (with a postcondition and optional implementation), or abstract (requiring overriding in extending types).

Constructors

Transparent (body : AstNode StmtExpr) : Body

A transparent body whose implementation is visible to callers.

Opaque (postconditions : List Condition)
  (implementation : Option (AstNode StmtExpr))
  (modifies : List (AstNode StmtExpr)) : Body

An opaque body with a postcondition, optional implementation, and modifies clause. Without an implementation the postcondition is assumed.

Abstract (postconditions : List Condition) : Body

An abstract body that must be overridden in extending types. A type containing any members with abstract bodies cannot be instantiated.

External : Body

An external body for procedures that are not translated to Core (e.g., built-in primitives).

5. Programs🔗

A Laurel program consists of procedures, global variables, type definitions, and constants.

🔗structure
Strata.Laurel.Program : Type
Strata.Laurel.Program : Type

A Laurel program consisting of static procedures, static fields, type definitions, and constants.

Constructor

Strata.Laurel.Program.mk

Fields

staticProcedures : List Procedure

Top-level procedures not attached to any type.

staticFields : List Field

Top-level fields (global variables).

types : List TypeDefinition

User-defined type definitions (composite and constrained).

constants : List Constant

Named constants.

6. Implementation🔗

The static semantics of Laurel are defined by Resolution.lean. This is where Laurel references are resolved and where type checking, when implemented, will be done. Calling resolve will produce diagnostics and a SemanticModel that can be used to navigate between definitions and references. If new references or definitions are created during compilation, resolve must be called again to get a complete model.

6.1. Translation Pipeline🔗

Laurel programs are verified by translating them to Strata Core and then invoking the Core verification pipeline. The Laurel compilation pipeline consists of three parts:

  • Lowering, consisting of many phases. Maps Laurel to Laurel

  • Ordering, consisting of a single pass. Maps Laurel to OrderedLaurel

  • Translation, consisting of a single pass. Maps OrderedLaurel to Core.

Ideally the translation pass only translates between types but does not change the structure of the program.

6.2. Lowering Passes🔗

The following passes are part of the lowering group:

  • TypeAliasElim: Eliminates type aliases by replacing all UserDefined references to alias names with their resolved target types. Chained aliases are resolved transitively. Alias entries are removed from the type list.

  • FilterNonCompositeModifies: Filters modifies clauses that refer to non-composite types (e.g. primitives), which cannot be heap-parameterized. Emits a warning for each removed clause. Should run before heap parameterization so that phase remains agnostic to modifies clauses.

  • EliminateValueInReturns: Rewrites return expr into outParam := expr; return for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns.

    • Comes before HeapParameterization because: eliminate value in returns need to come before any passes that change the amount of output parameters of procedures.

  • HeapParameterization: Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as Map Composite (Map Field Box). Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use readField and updateField functions.

    • Comes before TypeHierarchyTransform because: the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass.

    • Comes before ModifiesClausesTransform because: the modifies pass refers to several types and variables introduced by heap parameterization: Composite, Field, $heap_in, $heap.

    • Comes before LiftExpressionAssignments because: the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted.

  • TypeHierarchyTransform: Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains.

  • ModifiesClausesTransform: Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap.

  • InferHoleTypes: Annotates every verification hole (.Hole) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values.

    • Comes before EliminateDeterministicHoles because: eliminating deterministic holes relies on knowing the type of holes

  • EliminateDeterministicHoles: Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes InferHoleTypes has already annotated holes with types.

  • DesugarShortCircuit: Rewrites short-circuit boolean operators (&& and ||) into equivalent conditional expressions. This simplifies subsequent passes and the final translation to Core, which does not have short-circuit semantics built in.

    • Comes before LiftExpressionAssignments because: The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass.

  • LiftExpressionAssignments: Lifts assignments that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed.

  • MergeAndLiftReturns: Attempts to merge and lift returns so that only a single outer return remains, enabling the procedure to be more easily converted to a functional form.

  • ConstrainedTypeElim: Eliminates constrained types by replacing them with their base types and generating constraint-checking functions and witness procedures. Type tests against constrained types are rewritten to call the generated constraint function.

6.3. Pass Dependency Graph🔗

The following graph shows the ordering constraints between passes.

Dependency edges (A → B means A must run before B):

  • EliminateValueInReturns → HeapParameterization

    • eliminate value in returns need to come before any passes that change the amount of output parameters of procedures.

  • HeapParameterization → TypeHierarchyTransform

    • the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass.

  • HeapParameterization → ModifiesClausesTransform

    • the modifies pass refers to several types and variables introduced by heap parameterization: Composite, Field, $heap_in, $heap.

  • HeapParameterization → LiftExpressionAssignments

    • the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted.

  • InferHoleTypes → EliminateDeterministicHoles

    • eliminating deterministic holes relies on knowing the type of holes

  • DesugarShortCircuit → LiftExpressionAssignments

    • The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass.

Pipeline execution order:

1. TypeAliasElim
2. FilterNonCompositeModifies
3. EliminateValueInReturns → HeapParameterization
4. HeapParameterization → TypeHierarchyTransform → ModifiesClausesTransform → LiftExpressionAssignments
5. TypeHierarchyTransform
6. ModifiesClausesTransform
7. InferHoleTypes → EliminateDeterministicHoles
8. EliminateDeterministicHoles
9. DesugarShortCircuit → LiftExpressionAssignments
10. LiftExpressionAssignments
11. MergeAndLiftReturns
12. ConstrainedTypeElim

7. Differences between Laurel and Core🔗

7.1. Language design🔗

7.1.1. Parameter lists🔗

Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout).

At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: assign x, y := multiOutCall(a, b) Core uses the argument list to assign the output parameters, like this: multiOutCall(a, b, out x, out y)

In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, hasInout(inout x).

7.1.2. Assignments to fresh and existing declarations🔗

In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example:

var x: int;
var z: int;
assign x, var y: int, z := hasThreeOutputs()

In Core, when calling a procedure with multiple outputs, each output parameter must be assigned to an existing local variable. Example:

var x: int;
var y: int;
var z: int;
hasThreeOutputs(out x, out y, out z);

7.2. Implementation🔗

In Laurel, all verification concepts, such as assume statements, pre and postconditions, and transparency of procedures, are part of the language. In Core however, there is the concept of metadata. Concepts that relate to only one or a few analyses might not be considered concepts of the Core language, and will then be represented using metadata instead of being given a typed representation in the AST.