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. Translation Pipeline

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. Laurel tries to include any features that are common to those three languages.

Laurel enables doing various forms of verification:

  • Deductive verification

  • (WIP) Model checking

  • (WIP) Property based testing

  • (WIP) Data-flow analysis

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) Higher-order procedures and procedure types

  • (WIP) Parametric polymorphism

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

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.1. Implementation Choices🔗

A design choice that impacts the implementation of Laurel is that statements and expressions share a single implementation type, the StmtExpr. This reduces duplication for constructs like conditionals and variable declarations. Each StmtExpr has a user facing type, which for statement-like constructs could be void.

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 : Strata.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)) : StmtExpr

Apply a primitive operation to the given arguments.

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 representing an unknown expression.

  • 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: 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. Translation Pipeline🔗

Laurel programs are verified by translating them to Strata Core and then invoking the Core verification pipeline. The translation involves several passes, each transforming the Laurel program before the final conversion to Core.

6.1. Heap Parameterization🔗

The heap parameterization pass transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as Map Composite (Map Field Box), where Box is a tagged union with constructors for each primitive type.

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.

6.2. Modifies Clauses🔗

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

6.3. Lifting Expression Assignments🔗

The expression assignment lifting pass transforms assignments that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions.

6.4. Translation to Core🔗

The final translation converts Laurel types, expressions, statements, and procedures into their Strata Core equivalents. Procedures with bodies that only have constructs supported by Core expressions are translated to a Core function, while other procedures become Core procedures.