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

Inequality test.

Logical conjunction (eager).

Logical disjunction (eager).

Logical negation.

Logical implication (short-circuit).

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

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

Arithmetic negation. Works on Int and Float64.

Addition. Works on Int and Float64.

Subtraction. Works on Int and Float64.

Multiplication. Works on Int and Float64.

Euclidean division. Works on Int and Float64.

Euclidean modulus. Works on Int and Float64.

Truncation division.

Truncation modulus.

Less than. Works on Int and Real.

Less than or equal. Works on Int and Real.

Greater than. Works on Int and Real.

Greater than or equal. Works on Int and Real.

String concatenation.

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

A sequence of statements with an optional label for Exit.

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

postTest selects when the condition is tested relative to the body:

• false (default) — a pre-test loop (while): the condition is checked before the body, so the body may run zero times.

• true — a post-test loop (do … while): the body runs once before the condition is first checked, so it always runs at least once.

Invariants are checked at the loop head (before each body) in both cases. A post-test loop is lowered to the pre-test form by the EliminateDoWhile pass.

Exit a labelled block. Models break and continue statements.

Return from the enclosing procedure with an optional value.

An integer literal.

A boolean literal.

A string literal.

A decimal literal.

A bitvector literal with value and width.

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).

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

Java-style increment/decrement operator. The target must be a Local or Field Variable. As an expression, prefix form yields the new value (after the update) and postfix form yields the old value (before the update). As a statement the yielded value is discarded. Eliminated by the EliminateIncrDecrAndCompoundAssign pass before lifting imperative expressions.

C-style compound assignment (x += e, x -= e, x *= e, x /= e, x %= e), plus x ^= e for string concatenation (Laurel uses ^ for concat, OCaml-style, not bitwise XOR). Lowers to target := target op rhs and yields the new value. The target must be a Local or Field Variable. Invariant: op is one of Add/Sub/Mul/Div/Mod/StrConcat — the only operators the concrete-to-abstract translator ever constructs here. Downstream sites may treat any other Operation as a StrataBug. Eliminated by the EliminateIncrDecrAndCompoundAssign pass before lifting imperative expressions.

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

Call a static procedure by name with the given arguments. Primitive operators are calls too: x + y is a StaticCall to the built-in wrapper $add. See Operation.procName.

Create new object (new). typeArgs carries explicit instantiation arguments for a generic composite, e.g. new Box<int> → ref = Box, typeArgs = [int]. Empty for a non-generic new C (the common case and the pre-existing surface syntax), so the monomorphizer can read the concrete instantiation directly off the allocation site rather than recovering it from surrounding context.

Reference to the current object (this/self).

Reference equality test between two expressions.

Type cast: treat the target as the given type.

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

Call an instance method on a target object.

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

Check whether a variable has been assigned.

Refer to the value of value at an earlier program point.

label? names which earlier state:

• none — the procedure's native pre-state (Core's two-state old). This is the only form on the regular path; surface old(e) produces it.

• some h — a named earlier state h, so old reads that state rather than the procedure entry state. h is bound either by a Snapshot h earlier in the body or by a threaded Heap parameter.

Coroutine-only: refer to the value of value at the start of the current coroutine step. Surface form: oldGuarantee(value).

Outside a coroutine body it is a resolution error. The lowering depends on the path:

• Body path — the start-of-step heap is the previous yield's post-havoc snapshot (or procedure entry for the first yield), so it lowers to a labeled Old value (some $old_heap) reading the start-of-step Snapshot — the same lowering as an implicit old(...) inside a guarantees clause.

• Caller path — the start-of-step heap is resume's native entry state (H2), so it lowers to a plain Old value (no label) that push-old distributes onto the inout $heap.

The user uses this in body asserts and loop invariants where the framework needs to relate the current heap to the previous yield's resume point.

Coroutine-only: the old state of a two-state relies R(old, now) — the heap at the coroutine's most recent suspension (H1). Surface form: oldRelies(value). Unlike OldGuarantee (whose old heap is resume's native entry state), H1 is tracked by the caller per instance and threaded in as an explicit $h_rely_old : Heap parameter, so on the caller path oldRelies(e) lowers to Old e (some $h_rely_old) (no Core old, since relies become resume preconditions). Seeded to the current heap on the first resume, so R(H1, now) becomes R(H0, H0) there.

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

Assert a condition, generating a proof obligation. The optional summary is a human-readable description of the property being checked.

Assume a condition, restricting the state space.

Throw a value on the exceptional channel. The operand is unconstrained at the throw site; the thrown types are reconciled at each enclosing catch (typed at their least common ancestor) and against the procedure's declared throwsType. See the Exceptions section of the Laurel User Guide.

Structured exception handler: a body, an ordered list of catch clauses (tried first-match-wins), and an optional finally arm that runs on every exit path. See the Exceptions section of the Laurel User Guide.

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

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

Marker for abstract contracts. Makes the containing type abstract.

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

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.

Yield expression used inside coroutines.

Statement position: suspends the coroutine; the resumed value is dropped. Expression position (z := yield): suspends; evaluates to the value the next resume(co, v) sends in (type matches the coroutine's resumes binding).

To yield a value outward, the user assigns it to the coroutine's yields binding before the suspension: x := e; yield.

Resume a coroutine instance, optionally sending it a value. target evaluates to the coroutine instance to resume. value is the value sent into the coroutine (the binding for the yield expression that suspended it); none for a unit-valued resume. As a statement, the resumed value (the next yield's payload) is dropped; in expression position (x := resume(g, v)) it is bound to x.

Has-next test on a coroutine instance: has_next(co) evaluates to true iff co has not yet run to completion (its internal $pc has not reached the END state).

Lowering artifact (no surface syntax): capture the current state at this program point under the opaque label label, so a later Old e (some label) reads e against it.