Laurel User Guide

4.17. Programs🔗

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

🔗structure
Strata.Laurel.LaurelProgram : Type
Strata.Laurel.LaurelProgram : Type

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

Constructor

Strata.Laurel.LaurelProgram.mk

Fields

staticProcedures : List Strata.Laurel.Procedure

Top-level procedures not attached to any type.

staticFunctions : List Strata.Laurel.Procedure

Top-level functions. Empty in a front end's program; the Transparency pass fills it.

staticFields : List Strata.Laurel.Field

Top-level fields (global variables).

types : List Strata.Laurel.TypeDefinition

User-defined type definitions (see the TypeDefinition constructors).

constants : List Strata.Laurel.Constant

Named constants.

heapFields : List Strata.Laurel.HeapField

Fields of composite types, named Composite.field. Empty in a front end's program; LowerComposite fills it in place of the composites' own fields, and HeapParameterization clears it again.

4.17.1. File-scope globals🔗

A program-level var counter: int defines shared mutable state. Laurel lowers direct and transitive global effects to hidden parameters in declaration order; initial values come from the caller or runtime.

Supported: reads and writes in procedure bodies (including instance and transitive calls), current global values in contracts, and multiple globals alongside heap state.

Not yet supported (reported with source diagnostics):

  • Global-dependent old(...) expressions.

  • Globals in entry procedures, constants, or constrained-type predicates and witnesses.

  • Explicit inout/global interactions and global-writing invokeOn procedures.

  • Writes in restricted expressions, ambiguous bodiless postconditions, and unsupported multi-output call shapes.

A leading $ is reserved for compiler-generated names; see Reserved names.