3 Types🔗

Every Boogie expression has exactly one type, but functions, procedures, quantifiers, lambdas and map types may be parameterised over type variables. Functions and procedures are polymorphic only at the outside — their type parameters are all bound in one list at the declaration — but map types nest, so a map may take a polymorphic map as a domain type and the type system is therefore higher-rank (see Higher-rank map types). There is no subtyping and no implicit conversion. Distinct types denote disjoint sets of values; the only way to move a value between two types is an explicit function such as int(...) or real(...).

The material below follows sections 2 and 5 of This is Boogie 2, but the tool has moved on considerably since 2008: it has gained real, floating point, rounding modes, strings, regular expressions and algebraic datatypes; it has lost the paper’s finite modifier; it accepts nullary map types, and map types whose bound type variables occur only in the result, both of which the paper forbids; and the choice of type encoding for the prover is now made automatically. Every such divergence is called out where it arises.

3.1 The shape of a type🔗

Types are parsed by the following productions of Source/Core/BoogiePL.atg (semantic actions elided):

Type

= ( TypeAtom

| Ident [ TypeArgs ]

| MapType

) .

TypeAtom

= ( "int" | "real" | "bool" | "(" Type ")" ) .

TypeArgs

= ( TypeAtom [ TypeArgs ]

| Ident    [ TypeArgs ]

| MapType

) .

MapType

= [ TypeParams ] "[" [ Types ] "]" Type .

TypeParams

= "<" Idents ">" .

Types

= Type { "," Type } .

So syntactically there are exactly three things a type can be: a parenthesised type or one of the three keyword atoms; an identifier applied to zero or more type arguments; or a map type. Everything else — bitvectors, floats, rmode, string, regex, type variables, type constructors, type synonyms and datatypes — goes through the identifier case and is distinguished during name resolution, not during parsing. The grammar file says so explicitly at the TypeAtom production:

/* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */

UnresolvedTypeIdentifier.ResolveType in Source/Core/AST/AbsyType.cs resolves an identifier by trying, in order:

1. the built-in name patterns bvN, floatSeE, rmode, string, regex;

2. an enclosing type-variable binder;

3. a declared type constructor (arity must match exactly);

4. a declared type synonym (arity must match exactly);

5. otherwise undeclared type: N (replacing with "bool" to continue resolving).

The ident token allows a leading backslash, and the parser’s Ident production strips it, so \bv32 and bv32 are the same name. The pretty-printer (TokenTextWriter.SanitizeIdentifier) puts a backslash back in front of names it considers reserved — the keyword list plus anything matching bvN — which is why a printed program can contain \bv32 and \rmode; those still resolve to the built-in types when read back.

3.2 Primitive types🔗

3.2.1 bool, int and real🔗

bool, int and real are the only three type names that are keywords of the grammar. int is the mathematical integers (unbounded), and real is the mathematical reals. There is no automatic conversion between them; the expression-level functions int(...) and real(...) do the conversion explicitly.

3.2.2 Bitvector types🔗

bvN for any decimal N denotes an N-bit bitvector. bv0 is legal, and the only upper bound on the width is that N must fit in a 32-bit signed integer.

Because the name is matched textually, the name bvN is reserved: declaring a type constructor, type synonym or type variable with such a name is an error.

type \bv32;

boogie /noVerify types-bv-name-clash.bpl

types-bv-name-clash.bpl(1,5): Error: type name: bv32 is registered for bitvectors

1 name resolution errors detected in types-bv-name-clash.bpl

3.2.3 Floating-point types🔗

floatSeE denotes an IEEE-754 binary floating-point type with a significand of S bits (including the hidden bit) and an exponent of E bits. The name is recognised by the pattern float, digits, e, digits; the tool emits it to SMT-LIB as (_ FloatingPoint E S). So float24e8 is Float32 and float53e11 is Float64. Boogie does not check that S and E are sensible; float1e1 resolves without complaint.

Floating point is absent from the 2008 paper. See Bitvectors, floating point and rounding modes for the literals, the operators and the :builtin catalogue.

3.2.4 rmode🔗

rmode is the type of IEEE-754 rounding modes. Its values are the literals RNE, RNA, RTP, RTN and RTZ, each of which also has a long spelling (roundNearestTiesToEven, roundNearestTiesToAway, roundTowardPositive, roundTowardNegative, roundTowardZero). It is not in the paper.

3.2.5 string and regex🔗

string is the type of SMT-LIB strings and regex the type of regular expressions over them. Neither is in the paper. See Strings and regular expressions.

3.2.6 None of these take arguments🔗

The five name-recognised primitive types are all nullary, and applying one to a type argument is a resolution error with a distinct message for each:

const x: bv32 int;

const y: float24e8 int;

const z: rmode int;

const w: string int;

const v: regex int;

boogie /noVerify types-primitive-args.bpl

types-primitive-args.bpl(1,9): Error: bitvector types must not be applied to arguments: bv32

types-primitive-args.bpl(2,9): Error: float types must not be applied to arguments: float24e8

types-primitive-args.bpl(3,9): Error: rounding mode type must not be applied to arguments: rmode

types-primitive-args.bpl(4,9): Error: string type must not be applied to arguments: string

types-primitive-args.bpl(5,9): Error: regex type must not be applied to arguments: regex

5 name resolution errors detected in types-primitive-args.bpl

3.2.7 These names are not keywords🔗

Only bool, int and real are keywords. bvN, floatSeE, rmode, string and regex are ordinary identifiers that resolution happens to recognise first. Because the built-in patterns are tried before the symbol table is consulted, a user declaration of one of those names is accepted and then silently ignored — except for bvN, which is diagnosed as shown above. All four declarations below are dead:

type string;

type regex;

type rmode;

type float24e8;

const a: string;

const c: rmode;

axiom a == c;

boogie /noVerify types-shadowed-names.bpl

types-shadowed-names.bpl(9,8): Error: invalid argument types (string and rmode) to binary operator ==

1 type checking errors detected in types-shadowed-names.bpl

The error shows that a and c received the built-in string and rmode types; the four type declarations contributed nothing.

3.2.8 Types are disjoint🔗

No value belongs to two types, and the type checker refuses to compare values of different types even when they are all numeric:

const i: int;

const r: real;

const v: bv8;

axiom i == r;

axiom i == v;

axiom r == v;

boogie /noVerify types-disjoint.bpl

types-disjoint.bpl(5,8): Error: invalid argument types (int and real) to binary operator ==

types-disjoint.bpl(6,8): Error: invalid argument types (int and bv8) to binary operator ==

types-disjoint.bpl(7,8): Error: invalid argument types (real and bv8) to binary operator ==

3 type checking errors detected in types-disjoint.bpl

3.3 Type constructors🔗

A type constructor is declared with type. Declaring the same type name twice is an error unless one of the two declarations carries {:extern}; that rule is uniform across all five namespaces and is described in Top-level declarations. The grammar is:

UserDefinedTypes

= "type" { Attribute } UserDefinedType { "," UserDefinedType } ";" .

UserDefinedType

= Ident [ WhiteSpaceIdents ] [ "=" Type ] .

WhiteSpaceIdents

= Ident { Ident } .

Without the = part this declares a type constructor whose arity is the number of trailing identifiers. Those identifiers are counted, not bound: their names are irrelevant, may repeat, and cannot be referred to anywhere. The pretty-printer prints them back as _.

One type declaration may introduce several types at once, mixing constructors and synonyms, and the leading attributes apply to all of them:

type {:mark} A, B = int, C d, D e f = [e]f;

const a: A;

const b: B;

const c: C int;

const d: D int bool;

boogie /noVerify /env:0 /print:- types-decl-list.bpl

type {:mark} A;

type {:mark} B = int;

type {:mark} C _;

type {:mark} D e f = [e]f;

const a: A;

const b: B;

const c: C int;

const d: D int bool;

Boogie program verifier finished with 0 verified, 0 errors

Note that the constructor’s parameter names have been erased to _ while the synonym’s have been kept — for a synonym they really are binders.

Type constructors and type synonyms share one namespace; a name may be declared only once, and no type variable may shadow it (see Type variables).

3.3.1 Applying a type constructor🔗

Type arguments are supplied by juxtaposition, not by a bracketed list. Application is n-ary and greedy: although TypeArgs is a right-recursive production, every argument it reads is appended to the same flat list, so arguments are consumed for as long as possible, or until a map type is reached, and they are all handed to the identifier that started the application. Nesting requires parentheses. (The paper calls this "right associative", but nothing is nested: Barrel Barrel Wicket gives the first Barrel two arguments rather than one, as the paper’s own commentary on that example says.) The following all parse and resolve:

type Wicket;

type Barrel a;

type C a b;

const a: C Wicket Wicket;

const c: Barrel (Barrel Wicket);

const d: Barrel [int] Barrel Wicket;

const f: C Wicket (Barrel int);

const g: C Wicket [int]Barrel int;

const j: C ([int]Wicket) Wicket;

boogie /noVerify types-ctor-args.bpl

Boogie program verifier finished with 0 verified, 0 errors

Here d is Barrel ([int] (Barrel Wicket)) and g is C Wicket ([int] (Barrel int)): once the parser hits [, the rest of the phrase belongs to the map type’s result. Arity mismatches are caught during resolution:

type Wicket;

type Barrel a;

type C a b;

const b: Barrel Barrel Wicket;

const e: C Wicket Barrel int;

const i: C [int]Wicket Wicket;

boogie /noVerify types-ctor-arity-errors.bpl

types-ctor-arity-errors.bpl(5,9): Error: type constructor received wrong number of arguments: Barrel

types-ctor-arity-errors.bpl(6,9): Error: type constructor received wrong number of arguments: C

types-ctor-arity-errors.bpl(7,9): Error: type constructor received wrong number of arguments: C

3 name resolution errors detected in types-ctor-arity-errors.bpl

Only one error per declaration: once the arity check fails, resolution returns without visiting the arguments, so a further error inside them is not reported. The paper attributes the third error to Wicket rather than to C; the tool blames C, because [int]Wicket Wicket is parsed as the single map type [int] (Wicket Wicket), leaving C with one argument.

3.3.2 The paper’s finite modifier does not exist🔗

Section 2.0 of the paper gives the production type Attribute* finite? Id Id*; and explains that a type constructor not declared finite has infinitely many individuals. The current grammar has no finite, so the paper’s example declares a unary constructor named finite:

type finite RGBColor;

const unique red: RGBColor;

boogie /noVerify types-finite.bpl

types-finite.bpl(2,18): Error: undeclared type: RGBColor (replacing with "bool" to continue resolving)

1 name resolution errors detected in types-finite.bpl

Correspondingly there is no cardinality assumption in either direction. A nullary type constructor becomes an uninterpreted SMT sort and nothing more:

type Ref;

var a: [Ref]int;

procedure P(o: Ref)

modifies a;

{

a[o] := 1;

assert a[o] == 1;

}

boogie types-array-theory.bpl /proverLog:log.smt2

Boogie program verifier finished with 1 verified, 0 errors

and, from the generated log.smt2:

(declare-sort T@Ref 0)

(declare-fun a@0 () (Array T@Ref Int))

An axiom that pins a user type down to finitely many values is therefore neither rejected nor rendered vacuous; it is simply an axiom.

3.3.3 Built-in type constructors🔗

A type constructor carrying a :builtin string attribute is not declared to the prover at all; the string is used as its SMT-LIB sort name and the type arguments are passed along. This is how the standard library exposes SMT-LIB sequences:

type {:builtin "Seq"} Seq _;

function {:builtin "seq.empty"} Seq_Empty<T>(): Seq T;

function {:builtin "seq.len"} Seq_Len<T>(a: Seq T): int;

procedure P()

{

var s: Seq int;

s := Seq_Empty();

assert Seq_Len(s) == 0;

}

boogie types-builtin-ctor.bpl /proverLog:log.smt2

Boogie program verifier finished with 1 verified, 0 errors

and, from log.smt2 — note that there is no declare-sort for Seq:

(declare-fun s@0 () (Seq Int))

A :builtin constructor is also exempt from monomorphisation (Monomorphism and the type encoding).

3.3.4 Datatypes are type constructors🔗

datatype declares a type constructor together with its constructors. Its type parameters are written in angle brackets at the declaration, but the resulting type is applied by juxtaposition like any other constructor:

Datatype

= "datatype" { Attribute } Ident [ TypeParams ] "{" Constructors "}" .

datatype Pair<A, B> { Pair(fst: A, snd: B) }

type IntPair = Pair int int;

procedure P()

{

var p: IntPair;

var q: Pair bool int;

p := Pair(1, 2);

q := Pair(true, 2);

assert p->fst == 1 && q->snd == 2;

}

boogie types-datatype.bpl

Boogie program verifier finished with 1 verified, 0 errors

Datatypes are absent from the paper. See Algebraic datatypes.

3.4 Type synonyms🔗

Adding = Type to a type declaration makes it a synonym instead of a constructor. The identifiers before the = are then genuine binders: they must be pairwise distinct, they may be mentioned in the right-hand side, and they may equally well be ignored. The contrast with a constructor, whose parameter identifiers are only counted, is sharp:

type C a a a;

type S a a = int;

const x: C int bool int;

const y: S int bool;

boogie /noVerify types-param-names.bpl

types-param-names.bpl(2,9): Error: more than one declaration of type variable: a

1 name resolution errors detected in types-param-names.bpl

type Wicket;

type MySynonym a = int;

type ComplicatedInt = MySynonym (MySynonym bool);

type MultiSet a = [a]int;

type S a b = <g>[b, g]int;

const q: MultiSet Wicket;

const r: ComplicatedInt;

const p: S bool (S Wicket <g>[g]g);

boogie /noVerify types-synonyms.bpl

Boogie program verifier finished with 0 verified, 0 errors

A synonym is a pure abbreviation. Using one is exactly the same as writing out its expansion, with the arguments substituted for the parameters and the right-hand side’s bound type variables renamed to avoid capture:

type S a = <g>[g, a]int;

var x: S <g>[g]g;

var y: <d>[d, <g>[g]g]int;

procedure P()

modifies x, y;

{

x := y;

y := x;

}

boogie types-synonym-capture.bpl

Boogie program verifier finished with 1 verified, 0 errors

The g bound by S and the g inside the argument are different variables, so S <g>[g]g is <d>[d, <g>[g]g]int and the two assignments are well typed. Likewise a synonym and its expansion are interchangeable everywhere:

type Wicket;

type MultiSet a = [a]int;

var q: MultiSet Wicket;

var r: [Wicket]int;

procedure P()

modifies q, r;

{

q := r;

r := q;

}

boogie types-synonym-transparent.bpl

Boogie program verifier finished with 1 verified, 0 errors

Internally the synonym is kept as an annotation wrapped around the expansion (TypeSynonymAnnotation), which is why diagnostics still show the synonym form; every structural operation — equality, unification, substitution — looks through it.

Three things are rejected: a synonym applied to the wrong number of arguments, a cycle among synonym definitions, and a use whose expansion violates a restriction of the enclosing context.

type MySynonym a = int;

type Bogus = MySynonym MySynonym;

type Ping = [int]Pong;

type Pong = [int]Ping;

const c: <b>[MySynonym b]int;

boogie /noVerify types-synonym-errors.bpl

types-synonym-errors.bpl(2,23): Error: type synonym received wrong number of arguments: MySynonym

types-synonym-errors.bpl(3,5): Error: type synonym could not be resolved because of cycles: Ping (replacing body with "bool" to continue resolving)

types-synonym-errors.bpl(4,5): Error: type synonym could not be resolved because of cycles: Pong (replacing body with "bool" to continue resolving)

types-synonym-errors.bpl(5,9): Error: type variable must occur in map arguments: b

4 name resolution errors detected in types-synonym-errors.bpl

The last error is the paper’s point that expansion happens before the enclosing restriction is applied: MySynonym b expands to int, so the map type becomes <b>[int]int and b no longer occurs anywhere in it.

Parameterised type synonyms do not make a program polymorphic; because they are expanded before the monomorphism check sees them, a program whose only type parameters are synonym parameters is still monomorphic and gets the array theory (Monomorphism and the type encoding).

type MultiSet a = [a]int;

var x: MultiSet int;

procedure P()

modifies x;

{

x[0] := 1;

assert x[0] == 1;

}

boogie types-synonym-monomorphic.bpl /proverLog:log.smt2

Boogie program verifier finished with 1 verified, 0 errors

and in log.smt2:

(declare-fun x@0 () (Array Int Int))

3.5 Map types🔗

A map type is written as an optional list of bound type variables, then the domain types in square brackets, then the result type:

MapType

= [ TypeParams ] "[" [ Types ] "]" Type .

Maps are total: a map value assigns a result to every tuple of domain values. There is no notion of a partial or bounded map in the type system.

3.5.1 Arity🔗

The number of domain types is the map’s arity. [int, int]bool is a two-dimensional array; [int][int]bool is a one-dimensional array of one-dimensional arrays, and the two are different types. Selection and update must supply exactly the declared number of indices, and only a map may be selected from:

var a: [int, int]bool;

const x: int;

procedure P()

modifies a;

{

assert a[1];

assert x[3] == 1;

}

boogie /noVerify types-map-arity-errors.bpl

types-map-arity-errors.bpl(7,10): Error: wrong number of arguments in map select: 1 instead of 2

types-map-arity-errors.bpl(8,9): Error: map select applied to a non-map: x

2 type checking errors detected in types-map-arity-errors.bpl

3.5.2 Nullary map types🔗

The Types list inside the brackets is optional, so []T is a legal map type of arity zero. This is not mentioned in the paper and is easy to miss in the grammar. A nullary map has exactly one "cell": it is selected with m[] and updated with m[] := e or m[:= e].

var m: []int;

procedure P()

modifies m;

{

m[] := 12;

assert m[] == 12;

m := m[:= 30];

assert m[] == 30;

}

boogie types-nullary-map.bpl

Boogie program verifier finished with 1 verified, 0 errors

A nullary map is nevertheless a distinct type from its result type:

var m: []int;

var n: int;

procedure P()

modifies m, n;

{

m := n;

n := m;

}

boogie /noVerify types-nullary-map-distinct.bpl

types-nullary-map-distinct.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to []int)

types-nullary-map-distinct.bpl(8,2): Error: mismatched types in assignment command (cannot assign []int to int)

2 type checking errors detected in types-nullary-map-distinct.bpl

In the verification condition, however, a nullary map is its result type. Under the monomorphic type encoding, IAppliableTranslator in Source/VCExpr/Boogie2VCExpr.cs rewrites a select with no indices and no type arguments to the map itself, and a store with no indices to the stored value, so m: []int above is declared to the prover as a plain integer (excerpt from the prover log):

boogie types-nullary-map.bpl /proverLog:log.smt2

(declare-fun m@0 () Int)

(declare-fun m@1 () Int)

That collapse is specific to the monomorphic encoding; under /typeEncoding:p or /typeEncoding:a every value is boxed into the universal sort and the map is declared as T@U like anything else, with explicit MapType0Select and MapType0Store functions. Adding /typeEncoding:p to the command above will not show you that, however: the program is monomorphic, so the option is overridden (Monomorphism and the type encoding). The polymorphic encoding of a nullary map is only reachable when something else in the program is polymorphic.

3.5.3 Polymorphic map types🔗

A map type may bind type variables, listed in angle brackets before the domain. The paper also allows Unicode angle brackets; the current scanner does not — only < and > are accepted.

An empty binder list is omitted and the map is called monomorphic; a non-empty one makes it polymorphic. A polymorphic map is a single value that can be selected at many types:

type Wicket;

type Barrel a;

const m: [Barrel Wicket]Wicket;

const n: <a>[Barrel a]a;

const grid: [int, int]bool;

const curried: [int][int]bool;

procedure P(bi: Barrel int, bw: Barrel Wicket)

{

var i: int;

var w: Wicket;

i := n[bi];

w := n[bw];

assert grid[0, 0] == curried[0][0] || true;

}

boogie types-maps.bpl

Boogie program verifier finished with 1 verified, 0 errors

n[bi] has type int and n[bw] has type Wicket, from the same constant n.

3.5.4 Where a bound type variable must occur🔗

Each type variable bound by a map type must occur somewhere in the map type. The paper states the stronger rule that it must occur in the domain, and justifies it by the property that every map selection then has a unique type independent of context. The implementation does not enforce that: Type.CheckBoundVariableOccurrences accepts an occurrence in the result type as well.

type C a;

const ok1: <a>[int]a;

const ok2: <a>[a][a]int;

const bad1: <a,b>[]C a;

const bad2: <a>[a]<b>[int]int;

boogie /noVerify types-map-tyvar-occurrence.bpl

types-map-tyvar-occurrence.bpl(5,12): Error: type variable must occur in map arguments: b

types-map-tyvar-occurrence.bpl(6,18): Error: type variable must occur in map arguments: b

2 name resolution errors detected in types-map-tyvar-occurrence.bpl

ok1 is the paper’s canonical illegal type. Here it is accepted, and the consequence the paper warned about follows: the type of a selection from such a map is fixed by its context, and when the context does not fix it the type checker guesses and warns (see Type inference and type proxies). The idiom is common in practice — <a>[]a appears in Boogie’s own test suite — so this is a deliberate relaxation rather than an oversight.

bad1 shows the rule that does bite: b occurs neither in the (empty) domain nor in the result C a. bad2 shows that the check applies to each map type separately: the inner <b>[int]int mentions b nowhere.

Combining the two relaxations gives the polymorphic nullary map <a>[]a: a single cell that can hold a value of any type, and whose contents change type on each store.

var p: <a>[]a;

procedure P()

modifies p;

{

p[] := 12;

assert p[] == 12;

p[] := true;

assert p[];

}

boogie types-poly-nullary-map.bpl

Boogie program verifier finished with 1 verified, 0 errors

3.5.5 Canonical ordering of map type parameters🔗

Map types are compared up to renaming of their bound type variables, but the comparison is positional. To make positions canonical, resolution re-sorts a map type’s parameters into order of first occurrence in the domain types followed by the result type (Type.SortTypeParams). The declared order is discarded:

var m: <a,b>[b,a]int;

var n: int;

procedure P()

modifies n;

{

n := m;

}

boogie /noVerify types-map-tyvar-order.bpl

types-map-tyvar-order.bpl(7,2): Error: mismatched types in assignment command (cannot assign <b,a>[b,a]int to int)

1 type checking errors detected in types-map-tyvar-order.bpl

Note that the diagnostic reports <b,a>[b,a]int, not the <a,b> that was written. (Be careful reading /print output here: /print runs before resolution, so it shows the declared order, not the canonical one.)

A consequence is that two map types that differ only in the order of their binders are the same type, while two that differ in which binder the result uses are not:

var m: <a,b>[a,b]a;

var n: <a,b>[a,b]b;

var p: [int]int;

var q: <a>[a]int;

procedure P()

modifies m, n, p, q;

{

m := n;

p := q;

q := p;

}

boogie /noVerify types-map-inequality.bpl

types-map-inequality.bpl(9,2): Error: mismatched types in assignment command (cannot assign <a,b>[a,b]b to <a,b>[a,b]a)

types-map-inequality.bpl(10,2): Error: mismatched types in assignment command (cannot assign <a>[a]int to [int]int)

types-map-inequality.bpl(11,2): Error: mismatched types in assignment command (cannot assign [int]int to <a>[a]int)

3 type checking errors detected in types-map-inequality.bpl

A polymorphic map type never unifies with a monomorphic one, however it is instantiated: the number of binders must match before anything else is compared.

The canonical order also makes type synonyms interact with map types the way one would hope. Below, C2 a b expands to C b a, and after sorting both map types are the same type up to renaming:

type C a b;

type C2 b a = C a b;

function g0(<a,b>[C2 a b]int) returns (int);

const c1: <a,b>[C b a]int;

axiom g0(c1) == 0;

boogie /noVerify types-map-alpha.bpl

Boogie program verifier finished with 0 verified, 0 errors

3.5.6 Higher-rank map types🔗

A map may take another map — including a polymorphic one — as a domain type. Boogie’s type system is therefore higher-rank, although universal types exist only as part of map types and never on their own.

type ref;

const mapSet: <a>[<b>[b]a]bool;

const emptySet: <a>[a]bool;

axiom mapSet[emptySet] == true;

axiom mapSet[emptySet := false] != mapSet;

axiom emptySet[13 := true][13] == true;

axiom (forall f: <c>[c]int, x: ref :: mapSet[f] ==> f[x] >= 0);

boogie /noVerify types-higher-rank.bpl

Boogie program verifier finished with 0 verified, 0 errors

mapSet is the set of all maps that take anything to some fixed type a. Selecting mapSet at emptySet instantiates a to bool. The failures are more instructive than the successes:

const mapSet: <a>[<b>[b]a]bool;

axiom mapSet[5];

axiom (forall f: <c>[c]c :: mapSet[f]);

axiom mapSet[mapSet] == true;

boogie /noVerify types-higher-rank-errors.bpl

types-higher-rank-errors.bpl(3,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)

types-higher-rank-errors.bpl(4,35): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

types-higher-rank-errors.bpl(5,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)

3 type checking errors detected in types-higher-rank-errors.bpl

The second is the interesting one. Unifying <c>[c]c with <b>[b]a would require a to be the bound variable c, which would let a bound variable escape its binder. MapType.Unify explicitly checks for that: after unifying under freshly renamed binders it verifies that none of the fresh variables shows up in either operand’s free variables or in the resulting substitution, and fails if one does.

3.5.7 Map values🔗

There is no map literal in the grammar. A value of map type comes from a variable, constant or function whose declared type is a map, or from a lambda. A lambda’s type is the map type formed from its bound variables’ types and its body’s type, and a lambda may itself be polymorphic:

procedure P()

{

var f: [int]int;

var g: <a>[a]bool;

f := (lambda x: int :: x + 1);

g := (lambda<a> y: a :: true);

assert f[3] == 4;

assert g[true] && g[3];

}

boogie types-lambda.bpl

Boogie program verifier finished with 1 verified, 0 errors

See Lambda expressions for lambda lifting, and The standard library for MapConst and the pointwise map operations.

3.6 Type variables🔗

A type variable is an identifier bound by an enclosing binder. Six kinds of binder introduce type variables that are later instantiated, and they differ in what they require of the variables they bind.

• Map types — <a,b>[...].... Each variable must occur somewhere in the domain or result types; the list is re-sorted into order of occurrence.

• Functions — function f<a>(...) returns (...). Each variable must occur in an in-parameter or out-parameter type. The list is re-sorted the same way.

• Procedures — procedure P<a>(...) returns (...). Same rule, with the message type variable must occur in procedure arguments.

• Implementations — implementation P<b>(...). Same rule; the names need not match the procedure’s, but the count must.

• Binder expressions — forall, exists and lambda. Here there is no occurrence requirement at all; an unused type parameter is accepted and simply sorted to the end.

• Datatypes — datatype D<A,B> .... The count is the type constructor’s arity. There is no occurrence requirement here either: a parameter no field mentions is accepted.

Type synonym parameters are binders too, but they are substituted away rather than instantiated, and they carry no occurrence requirement.

The occurrence rule for functions and procedures allows a variable that appears only among the results:

procedure P<a>(x: int, y: bool) returns (z: int, w: bool);

procedure Q<a>(x: int, y: bool) returns (z: int, w: a);

boogie /noVerify types-proc-tyvars.bpl

types-proc-tyvars.bpl(1,10): Error: type variable must occur in procedure arguments: a

1 name resolution errors detected in types-proc-tyvars.bpl

An implementation may rename its procedure’s type parameters but must declare the same number of them:

procedure Q<a>(x: a) returns (y: a);

implementation Q<b>(x: b) returns (y: b)

{

y := x;

}

procedure R<a>(x: a) returns (y: a);

implementation R(x: int) returns (y: int)

{

y := x;

}

boogie /noVerify types-impl-tyvars.bpl

types-impl-tyvars.bpl(10,15): Error: mismatched number of type parameters in procedure implementation: R

1 type checking errors detected in types-impl-tyvars.bpl

3.6.1 Scope and shadowing🔗

Type variables live in their own scope stack, but the rules are strict:

• A type variable may not have the same name as any declared type constructor or type synonym — even though the constructor could never be referred to from inside the binder anyway.

• A type variable may not shadow an enclosing type variable of the same name. Nesting two binders that use the same name is an error, not shadowing.

• A type variable may not be named bvN.

type Ref;

type MySyn = int;

const c: <Ref>[Ref]int;

const d: <a>[<a>[a]int]int;

function f<MySyn>(x: MySyn) returns (int);

boogie /noVerify types-tyvar-clash.bpl

types-tyvar-clash.bpl(4,10): Error: name is already reserved for type constructor: Ref

types-tyvar-clash.bpl(5,14): Error: more than one declaration of type variable: a

types-tyvar-clash.bpl(6,11): Error: name is already reserved for type constructor: MySyn

3 name resolution errors detected in types-tyvar-clash.bpl

The third message says "type constructor" although MySyn is a synonym; constructors and synonyms share one table and the message does not distinguish them.

Type variables occupy a namespace disjoint from ordinary variables, constants and functions, so a type variable named x and a value named x can coexist.

3.7 Type checking🔗

Type checking is described in section 5 of the paper. Most of it is unsurprising — the boolean connectives take and return bool, arithmetic takes and returns int or real, and so on; see Type checking of expressions. The interesting rules are the ones that involve instantiating type parameters, and they all share one mechanism.

3.7.1 The mechanism: matching by unification🔗

Whenever Boogie applies something with formal type parameters a — a function, a procedure, or a polymorphic map — it does the following (Type.MatchArgumentTypes and Type.CheckArgumentTypes in AbsyType.cs):

1. Replace each formal type parameter by a fresh type proxy, an as-yet-unknown type, giving a substitution s.

2. For each argument position, unify the substituted formal type with the actual argument’s type. A failure is reported as invalid type for argument i in ...: A (expected: F).

3. Apply s to the formal result type(s) to get the actual result type(s).

4. If any error occurred and some formal type parameter still occurs free in the result, give up on the result type entirely (returning null) so that the surrounding expression does not produce a cascade of spurious errors. If the result is fully determined despite the error, return it and carry on.

Unification is ordinary first-order unification with an occurs check, extended to look through type synonyms, to compare map types up to renaming of their binders, and to reject substitutions that would let a bound variable escape. Only the formal type parameters (and unresolved proxies) are unifiable; a type variable bound elsewhere behaves as a rigid constant.

3.7.2 Map selection🔗

Paper rule: if a has type <x>[U]V, and there is a substitution s with domain exactly x such that each index bi has type Uis, then a[b] has type Vs.

Equivalently: the map’s binders are the only unifiable variables; the index types determine them; the result is the map’s result type under that instantiation. If the map type is not polymorphic the substitution is empty and this is ordinary array indexing.

3.7.3 Map update🔗

Paper rule: if a has type <x>[U]V, s has domain exactly x, each index bi has type Uis and the right-hand side e has type Vs, then a[b := e] has type <x>[U]V — the map type, unchanged. Updating a polymorphic map at one instantiation does not make it monomorphic.

The paper’s heap encoding exercises both rules:

type Ref;

type Field a;

type HeapType = <a>[Ref, Field a]a;

var Heap: HeapType;

const unique C.data: Field int;

const unique C.next: Field Ref;

const unique alloc: Field bool;

procedure P(o: Ref)

modifies Heap;

{

var i: int;

var b: bool;

i := Heap[o, C.data];

b := Heap[o, alloc];

Heap := Heap[o, C.data := i + 1];

assert Heap[o, C.data] == i + 1;

assert Heap[o, alloc] == b;

}

boogie types-heap.bpl

Boogie program verifier finished with 1 verified, 0 errors

Heap[o, C.data] instantiates a to int from the second index and yields int; Heap[o, alloc] instantiates it to bool. The store keeps Heap at type HeapType. When the instantiation cannot be made consistent the error names the offending position:

type Ref;

type Field a;

var Heap: <a>[Ref, Field a]a;

const unique C.data: Field int;

procedure P(o: Ref)

modifies Heap;

{

var b: bool;

b := Heap[o, C.data];

Heap := Heap[o, C.data := true];

Heap := Heap[C.data, o := 3];

}

boogie /noVerify types-heap-errors.bpl

types-heap-errors.bpl(11,2): Error: mismatched types in assignment command (cannot assign int to bool)

types-heap-errors.bpl(12,28): Error: right-hand side in map store with wrong type: bool (expected: int)

types-heap-errors.bpl(13,15): Error: invalid type for argument 0 in map store: Field int (expected: Ref)

types-heap-errors.bpl(13,23): Error: invalid type for argument 1 in map store: Ref (expected: Field a)

4 type checking errors detected in types-heap-errors.bpl

Line 11 is not a select error: the select itself is fine and produces int, and only the assignment complains. That is the "carry on with a fully determined result" branch of the algorithm at work.

3.7.4 Function and procedure application🔗

Paper rule: if f<x>(U) returns (V) is in scope, s has domain exactly x, and each argument ai has type Uis, then f(a) has type Vs.

type ref;

type Field a;

function fieldValue<a>(ref, Field a) returns (a);

const intField: Field int;

const refField: Field ref;

const obj: ref;

const someInt: int;

axiom someInt == fieldValue(obj, intField);

axiom someInt == fieldValue(fieldValue(obj, refField), intField);

axiom someInt == fieldValue(obj, fieldValue(obj, refField));

boogie /noVerify types-poly-function.bpl

types-poly-function.bpl(13,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)

1 type checking errors detected in types-poly-function.bpl

Note the nesting in the second axiom: the inner fieldValue(obj, refField) instantiates a to ref and yields a ref, which the outer call then uses as its first argument. Each application gets its own instantiation.

A call matches the procedure’s out-parameters against the assignment targets in the same pass, so the targets participate in choosing the instantiation and can be the thing that fails:

type ref;

type Field a;

procedure FieldAccess<b>(heap: <a>[ref, Field a]a, obj: ref, f: Field b)

returns (res: b);

procedure UseHeap(heap: <a>[ref, Field a]a, obj: ref)

{

var f1: Field int;

var f2: Field bool;

var x: int;

var y: bool;

call x := FieldAccess(heap, obj, f1);

call y := FieldAccess(heap, obj, f2);

call y := FieldAccess(heap, obj, f1);

call x := FieldAccess(heap, obj, obj);

}

boogie /noVerify types-call-outparams.bpl

types-call-outparams.bpl(16,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)

types-call-outparams.bpl(17,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)

2 type checking errors detected in types-call-outparams.bpl

The first two calls succeed with b instantiated to int and to bool respectively. Note that in-parameters are matched before out-parameters, which is why the third call blames the result rather than f1.

3.7.5 Equality🔗

Equality is type checked liberally. a == b is well typed if there is any instantiation of the free type variables of the two operand types that makes them equal — the operands’ free type variables are all treated as unifiable, not just the type parameters of some application. The semantics of a == b is that the two sides evaluate to the same value and the same type.

type Field a;

const F0: Field int;

const F1: Field bool;

function LiberalEqual<a,b>(a, b) returns (bool);

function StrictEqual<a>(a, a) returns (bool);

axiom LiberalEqual(F0, F1);

axiom StrictEqual(F0, F0);

axiom (forall<a> f: Field a :: f == F0);

axiom F0 == F1;

axiom StrictEqual(F0, F1);

boogie /noVerify types-equality.bpl

types-equality.bpl(11,9): Error: invalid argument types (Field int and Field bool) to binary operator ==

types-equality.bpl(12,22): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)

2 type checking errors detected in types-equality.bpl

f == F0 is accepted because a can be instantiated to int; F0 == F1 is rejected because Field int and Field bool have no free type variables and are simply different. Note also the difference between the two helper functions: LiberalEqual<a,b> accepts anything, whereas StrictEqual<a> forces both arguments to the same type, which is a common idiom for getting equality-like typing rules out of a user-declared function.

3.7.6 Type inference and type proxies🔗

Boogie infers types only within an expression; every declaration must be fully annotated. An unknown type during checking is a TypeProxy, a mutable cell that unification fills in. Three flavours exist:

• TypeProxy — completely unknown.

• MapTypeProxy — known to be a map of a given arity, contents unknown.

• BvTypeProxy — known to be a bitvector of at least n bits, possibly with constraints recording that it is the concatenation of two other bitvector types.

After type checking, TypeAmbiguitySeeker walks the program looking for proxies that were never resolved. Rather than reporting an error it instantiates each one and emits a warning:

• a bare proxy becomes int;

• a bitvector proxy becomes bvn for its minimum width;

• a map proxy of arity k becomes <arg0,...,argk-1,res>[arg0,...,argk-1]res — a fully polymorphic map, which incidentally is a type the paper’s rules would reject, since res occurs only in the result.

type Set a;

function EmptySet<a>() returns (Set a);

function Card<a>(Set a) returns (int);

function Gimmie<T>() returns (T);

procedure P()

{

var c: int;

var b: bool;

assert Card(EmptySet()) >= 0 || true;

c := Gimmie()[3];

b := Gimmie()[7:0] == 0bv7;

}

boogie /noVerify types-ambiguous.bpl

types-ambiguous.bpl(10,9): Warning: type parameter a is ambiguous, instantiating to int

types-ambiguous.bpl(11,7): Warning: type parameter T is ambiguous, instantiating to <arg0,res>[arg0]res

types-ambiguous.bpl(12,7): Warning: type parameter T is ambiguous, instantiating to bv7

Boogie program verifier finished with 0 verified, 0 errors

These are warnings, not errors, and the program continues to verification with the guessed types. Treat them as a signal that the program does not mean what you think it means.

3.7.7 Type ascription🔗

An expression can be annotated with a type using :. This is an ascription, not a cast: the ascribed type is unified with the expression’s type, so it can only pin down otherwise-undetermined type parameters, never convert.

type Set a;

function EmptySet<a>() returns (Set a);

function Card<a>(Set a) returns (int);

procedure P()

{

assert Card(EmptySet() : Set bool) >= 0 || true;

assert (3 : bool) == true;

}

boogie /noVerify types-ascription.bpl

types-ascription.bpl(8,12): Error: int cannot be coerced to bool

1 type checking errors detected in types-ascription.bpl

The first assertion produces no ambiguity warning: the ascription supplied the instantiation. The second shows that ascription cannot change a type.

The grammar file warns about a parsing hazard here: a type can begin with <, but < is also a relational operator, and the parser prefers to read a map type.

type C;

const c: int;

axiom 5 : C < 0;

boogie /noVerify types-ascription-parse.bpl

types-ascription-parse.bpl(3,15): error: invalid Ident

1 parse errors detected in types-ascription-parse.bpl

3.8 Monomorphism and the type encoding🔗

How types reach the SMT solver depends on whether the program is monomorphic. MonomorphismChecker in Source/Core/Monomorphization.cs answers that question. A program is monomorphic exactly when none of the following occurs:

• a function, procedure, implementation or datatype constructor with a non-empty type parameter list;

• a forall, exists or lambda with a non-empty type parameter list;

• a map type with a non-empty type parameter list;

• a type constructor declaration of arity greater than zero that does not carry a :builtin attribute.

Note the last two points. A parameterised type synonym does not count, because synonyms are expanded before the check sees them; and a :builtin constructor such as the standard library’s Seq does not count, because the prover already knows how to handle it.

ExecutionEngine.ResolveAndTypecheck then dispatches:

• If the program is monomorphic, the type encoding is forced to monomorphic, overriding whatever /typeEncoding says. Map types become SMT-LIB arrays (or uninterpreted sorts with select/store axioms if /useArrayAxioms is given), and each type constructor instance becomes its own uninterpreted sort.

• Otherwise, if the encoding is monomorphic (the default), the Monomorphizer tries to specialise the program. Success proceeds as above; failure is fatal and reports either unhandled polymorphic features detected or expanding type cycle detected.

• Otherwise (/typeEncoding:p or /typeEncoding:a) the polymorphic encoding is used, everything is boxed into a universal sort, and maps are axiomatised rather than using the array theory. Datatypes and :define functions are not supported in that mode.

3.8.1 Monomorphic programs🔗

The excerpts below are from the generated log.smt2.

type Ref;

var a: [Ref]int;

procedure P(o: Ref)

modifies a;

{

a[o] := 1;

assert a[o] == 1;

}

boogie types-array-theory.bpl /proverLog:log.smt2

(declare-sort T@Ref 0)

(declare-fun a@0 () (Array T@Ref Int))

boogie /useArrayAxioms types-array-theory.bpl /proverLog:log.smt2

(declare-sort T@Ref 0)

(declare-sort |T@[Ref]Int| 0)

(declare-fun a@0 () |T@[Ref]Int|)

Adding /typeEncoding:p to the first command changes nothing, because monomorphic detection overrides the option.

3.8.2 Monomorphisable programs🔗

A polymorphic program that can be specialised is rewritten so that each used instantiation becomes its own declaration:

type Set a;

function EmptySet<a>() returns (Set a);

function Card<a>(Set a) returns (int);

procedure P()

{

var s: Set int;

var t: Set bool;

s := EmptySet();

t := EmptySet();

assert Card(s) == Card(t) || true;

}

boogie types-monomorphizable.bpl /proverLog:log.smt2

Boogie program verifier finished with 1 verified, 0 errors

(declare-sort T@Set_30 0)

(declare-fun s@0 () T@Set_30)

(declare-fun EmptySet_30 () T@Set_30)

(declare-sort T@Set_34 0)

(declare-fun t@0 () T@Set_34)

(declare-fun EmptySet_34 () T@Set_34)

(declare-fun Card_30 (T@Set_30) Int)

(declare-fun Card_34 (T@Set_34) Int)

Set int and Set bool have become two unrelated nullary sorts, and EmptySet and Card two copies each. (The numeric suffixes are internal counters and are not stable across versions.)

3.8.3 When monomorphisation fails🔗

MonomorphizableChecker reports two distinct failures.

Unhandled polymorphism means a type proxy survived type checking with no instantiation — typically a polymorphic call in a position the type checker does not constrain, such as inside an attribute:

procedure B()

{

assume {:add_to_pool "A", MapConst(false)} true;

}

boogie /lib:base types-unhandled-polymorphism.bpl

Unable to monomorphize input program: unhandled polymorphic features detected

Expanding type cycle means the instantiations would not terminate. The checker builds a graph whose nodes are type variables, with an edge from T to U when T flows into U at a call or function application, and marks the edge strong when what flows is a type constructed from T rather than T itself. If any strongly connected component contains a strong edge, the set of needed instantiations is infinite:

type Box a;

procedure A<T>(i: T)

{

var b: Box T;

call A(b);

}

boogie types-expanding-cycle.bpl

Unable to monomorphize input program: expanding type cycle detected

Both failures are fatal — nothing is verified. The escape hatch is to ask for a polymorphic encoding explicitly:

boogie /typeEncoding:p types-expanding-cycle.bpl

Boogie program verifier finished with 1 verified, 0 errors

The shape of the three encodings at the solver is in Type encodings and monomorphisation.

3.8.4 Datatypes and :define require the monomorphic encoding🔗

If the program is polymorphic and a non-monomorphic encoding was requested, datatypes and functions carrying :define are rejected outright:

boogie /typeEncoding:p types-datatype.bpl

Datatypes only supported with monomorphic encoding

type Box a;

function {:define} f(x: int) : int { x + 1 }

procedure A<T>(i: T)

{

var b: Box T;

assert f(1) == 2;

}

boogie /typeEncoding:p types-define-encoding.bpl

Functions with :define attribute only supported with monomorphic encoding

Both checks are reached only when the program is not monomorphic. A datatype of arity zero does not make a program polymorphic, so boogie /typeEncoding:p on a program whose only datatype is datatype Color { Red(), Green() } verifies normally — the monomorphic encoding is selected regardless of the option.

3.9 Divergences from This is Boogie 2🔗

• New primitive types. real, floatSeE, rmode, string and regex did not exist in 2008. The paper’s TypeAtom production lists only bool, int and the bitvectors.

• No finite. The paper’s finite modifier on type constructors is not in the grammar, and there is no cardinality assumption on user types.

• Nullary map types. []T is legal and is undocumented; under the monomorphic encoding it is represented by T in the verification condition.

• Result-only type variables. The paper requires each map type variable to occur in the domain; the tool also accepts occurrence in the result, so <a>[int]a and <a>[]a are legal. The paper’s claim that every map selection has a context-independent type therefore no longer holds; ambiguity is resolved by a warning and a default.

• No Unicode angle brackets. The paper allows ⟨ and ⟩ as alternatives to < and >; the scanner does not.

• Datatypes. datatype declarations, which introduce type constructors with angle-bracketed parameters, postdate the paper.

• Type encoding. The paper does not discuss monomorphisation. The tool now detects monomorphic programs, monomorphises polymorphic ones by default, and only falls back to the predicate or argument encodings when asked.