▼The Boogie Language:   A Reference
►11 The standard library
On this page:
11.1 Loading a library
11.1.1 Automatic loading for Civl programs
11.1.2 Monomorphisation
11.2 Map combinators
11.2.1 Implementation note:   the emitted SMT
11.2.2 Integer ranges
11.3 Default
11.4 Option, Unit and Unit  Map
11.5 Sets
11.5.1 Set cardinality:   /  lib:  set_  size
11.6 Vectors
11.6.1 Representation
11.6.2 The canonicalisation axioms
11.6.3 Vector operations
11.6.4 Concat and Slice
11.6.5 Extensionality:   Vec_  Ext
11.7 Sequences
11.8 Finite maps
11.8.1 Operations
11.8.2 Permission collectors
11.9 Civl-oriented types and primitives
11.9.1 One, Cell, Tag, Loc
11.9.2 The linear primitives
11.9.3 Surprise:   Map_  Put assumes freshness of a linear key
11.9.4 Allocation:   Loc_  New, Tag_  New, Tags_  New
11.9.5 Move, Copy, Assume, Assert
11.9.6 Map well-formedness is free in Civl
11.10 The node library
11.10.1 Node, Between and Avoiding
11.10.2 In  Domain
11.10.3 Stack, set and queue abstractions
11.10.4 The lemmas are trusted unless you discharge them
11.11 Divergences from This is Boogie 2
11.12 Where to find real usage
8.17
    contents    up   

11 The standard library🔗

Boogie ships with three small libraries that are not part of the language but are compiled into the tool as embedded resources and can be pulled into a program on demand. They are the closest thing Boogie has to a prelude: maps lifted pointwise, sets, finite maps, an Option type, a vector datatype, SMT sequences, and the datatypes and primitives that the Civl concurrency layer builds on.

None of this exists in This is Boogie 2 (2008). The paper predates datatypes, and therefore predates every datatype in these files. Everything in this chapter is documented from the library sources (Source/Core/base.bpl, node.bpl, set_size.bpl) and from the C# that gives some of the declarations extra meaning.

The libraries are ordinary Boogie text. Nothing in them is privileged by the parser: they are parsed, resolved and typechecked exactly like your own declarations, and they land in the same global namespace. A handful of the declarations are privileged after that point — the {:builtin} functions are translated directly to SMT operators, and the linear primitives at the end of base.bpl are rewritten by the Civl front end into assertions and assignments. Those cases are called out below.

11.1 Loading a library🔗

boogie /help

/lib:<name>   Include definitions in library <name>. The file <name>.bpl

              must be an included resource in Core.dll. Currently, the

              following libraries are supported---base, node.

That is the whole of the tool’s own documentation for the feature. There are three libraries:

Nothing is loaded unless you ask for it. With load.bpl containing

procedure p(v: Vec int)

{

  assert Vec_Len(v) >= 0;

}

the library names are simply undeclared:

boogie load.bpl

load.bpl(1,15): Error: undeclared type: Vec (replacing with "bool" to continue resolving)

load.bpl(1,15): Error: undeclared type: Vec (replacing with "bool" to continue resolving)

load.bpl(3,9): Error: use of undeclared function: Vec_Len

3 name resolution errors detected in load.bpl

boogie /lib:base load.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

The name after /lib: is turned into the resource name Core.<name>.bpl and looked up in Boogie.Core.dll. A name that does not resolve produces a message and no declarations:

boogie /lib:vec load.bpl

Error locating library: Core.vec.bpl not found

Nothing else is printed — the run stops there and verifies nothing — yet Boogie still exits with status 0, like every other failure that is not a command-line error (Exit codes). A misspelled /lib: name in a build script is therefore silent.

The libraries are appended to the program after all command-line .bpl files have been parsed, and everything is resolved together. Consequences:

Loading node without base, against the same load.bpl, produces 186 errors; here are the first four and the last:

boogie /lib:node load.bpl

node.bpl(1,30): Error: undeclared type: Option (replacing with "bool" to continue resolving)

load.bpl(1,15): Error: undeclared type: Vec (replacing with "bool" to continue resolving)

load.bpl(1,15): Error: undeclared type: Vec (replacing with "bool" to continue resolving)

load.bpl(3,9): Error: use of undeclared function: Vec_Len

...

186 name resolution errors detected in load.bpl

A clash looks like this. With clash.bpl containing

function Default<T>(): T;

procedure p() { }

boogie /lib:base clash.bpl

base.bpl(31,9): Error: more than one declaration of function name: Default

1 name resolution errors detected in clash.bpl

11.1.1 Automatic loading for Civl programs🔗

If any top-level declaration in the program carries a Civl attribute — {:layer}, {:yields}, {:hide}, {:sync}, {:linear}, {:linear_in} or {:linear_out} — then base is added to the library set automatically and /inferModifies is turned on. So Civl programs never need /lib:base on the command line, and most of the samples in Test/civl/ do not pass it.

The check inspects only the attributes of the top-level declaration itself, not of its formal parameters. A procedure whose only Civl marking is on a parameter therefore does not trigger the automatic load:

procedure P({:linear} x: One int)

{

}

boogie linear-formal.bpl

linear-formal.bpl(1,25): Error: undeclared type: One (replacing with "bool" to continue resolving)

linear-formal.bpl(1,25): Error: undeclared type: One (replacing with "bool" to continue resolving)

2 name resolution errors detected in linear-formal.bpl

Adding /lib:base fixes it. A yield procedure {:layer 1} in the same program would also fix it, because {:layer} sits on the declaration.

11.1.2 Monomorphisation🔗

Boogie’s default type encoding is monomorphic. A program that is already monomorphic is used as it stands; anything else is run through the monomorphisation pass, and a program the monomorphiser cannot handle is a fatal error. Almost every declaration in the libraries is polymorphic — in base.bpl only Identity and its axiom, AtLeast, Range, Loc, Unit, Assume and Assert are not, and node.bpl and set_size.bpl are polymorphic throughout — and the {:builtin} map functions only make sense once the type arguments are known — MapConst is emitted as SMT ((as const (Array Int Bool)) ...), which requires a concrete array sort. Loading a library therefore guarantees that you go through that pass:

procedure A<T>(i: T)

{

    call A(Some(i));

}

boogie /lib:base mono-cycle.bpl

Unable to monomorphize input program: expanding type cycle detected

This is not something the libraries introduce, though; the same failure occurs for any polymorphic program that grows its type arguments, with no library loaded at all:

procedure A<T>(i: T)

{

  var m: [int]T;

  call A(m);

}

boogie mono-nolib.bpl

Unable to monomorphize input program: expanding type cycle detected

11.2 Map combinators🔗

base.bpl opens with functions that lift scalar operations pointwise over maps. All of them are declared {:builtin "..."} and are translated directly into SMT array combinators; none of them has a Boogie-level axiomatisation.

function {:builtin "MapConst"} MapConst<T,U>(U): [T]U;

function {:builtin "MapEq"} MapEq<T,U>([T]U, [T]U) : [T]bool;

function {:builtin "MapIte"} MapIte<T,U>([T]bool, [T]U, [T]U) : [T]U;

 

function {:builtin "MapOr"} MapOr<T>([T]bool, [T]bool) : [T]bool;

function {:builtin "MapAnd"} MapAnd<T>([T]bool, [T]bool) : [T]bool;

function {:builtin "MapNot"} MapNot<T>([T]bool) : [T]bool;

function {:builtin "MapImp"} MapImp<T>([T]bool, [T]bool) : [T]bool;

function {:builtin "MapIff"} MapIff<T>([T]bool, [T]bool) : [T]bool;

function {:inline} MapDiff<T>(a: [T]bool, b: [T]bool) : [T]bool

{

  MapAnd(a, MapNot(b))

}

 

function {:builtin "MapAdd"} MapAdd<T>([T]int, [T]int) : [T]int;

function {:builtin "MapSub"} MapSub<T>([T]int, [T]int) : [T]int;

function {:builtin "MapMul"} MapMul<T>([T]int, [T]int) : [T]int;

function {:builtin "MapDiv"} MapDiv<T>([T]int, [T]int) : [T]int;

function {:builtin "MapMod"} MapMod<T>([T]int, [T]int) : [T]int;

function {:builtin "MapGt"} MapGt<T>([T]int, [T]int) : [T]bool;

function {:builtin "MapGe"} MapGe<T>([T]int, [T]int) : [T]bool;

function {:builtin "MapLt"} MapLt<T>([T]int, [T]int) : [T]bool;

function {:builtin "MapLe"} MapLe<T>([T]int, [T]int) : [T]bool;

 

function {:inline} Id<T>(t: T): T

{

  t

}

Read them as follows, for every index i of the domain type:

procedure MapOps()

{

  var a, b: [int]bool;

  var m, n: [int]int;

 

  assert MapConst(true) == (MapNot(MapConst(false)): [int]bool);

  assert MapAnd(a, b) == MapNot(MapOr(MapNot(a), MapNot(b)));

  assert MapAdd(m, n) == MapAdd(n, m);

  assert MapIte(a, m, n)[3] == (if a[3] then m[3] else n[3]);

  assert MapLe(m, n)[7] == (m[7] <= n[7]);

  assert MapDiv(m, n)[3] == m[3] div n[3];

  assert MapMod(m, n)[3] == m[3] mod n[3];

  assert MapDiff(a, b) == MapAnd(a, MapNot(b));

  assert MapEq(m, n)[0] == (m[0] == n[0]);

  assert Id(a) == a;

}

boogie /lib:base mapops.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

Five of those assertions compare whole maps rather than elements. Two of them (MapDiff and Id) are syntactic identities once the {:inline} bodies are substituted, but the other three — MapConst/MapNot, De Morgan on MapAnd, and commutativity of MapAdd — only work because Boogie’s current SMT encoding gives maps extensionality. The 2008 paper explicitly says it does not: "Maps do not necessarily satisfy extensionality [...] For example, extensionality would imply b[j := b[j]] == b, but this property does not necessarily hold in Boogie." It holds now, with no library at all. The whole Set_* layer below depends on this: Set_IsSubset is defined as MapImp(a, b) == MapConst(true), which is useless without extensionality.

11.2.1 Implementation note: the emitted SMT🔗

The builtin names are recognised by the SMT-LIB lineariser, which rewrites them into Z3 array combinators: MapConst becomes (as const <sort>), MapAnd becomes (_ map and), MapAdd becomes (_ map (+ (Int Int) Int)), and so on.

11.2.2 Integer ranges🔗

Three declarations in the middle of base.bpl exist to build integer ranges out of the combinators. They are used by the Vec axioms but are public and generally useful.

const Identity: [int]int;

axiom (forall x: int :: Identity[x] == x);

 

function {:inline} AtLeast(x: int): [int]bool

{

  MapLe(MapConst(x), Identity)

}

function {:inline} Range(from: int, n: int): [int]bool {

  MapDiff(AtLeast(from), AtLeast(from + n))

}

AtLeast(x) is the set of integers >= x; Range(from, n) is the half-open interval [from, from+n), and is empty when n <= 0.

procedure Ranges()

{

  assert Identity[7] == 7;

  assert AtLeast(3)[3] && AtLeast(3)[100] && !AtLeast(3)[2];

  assert Range(3, 2) == MapConst(false)[3 := true][4 := true];

  assert Range(0, 0) == MapConst(false);

  assert Range(5, -1) == MapConst(false);

}

boogie /lib:base ranges.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

11.3 Default🔗

function Default<T>(): T;

An uninterpreted nullary function, one per instantiated type. It is a function, so it is deterministic, but no axiom pins down its value: Default(): int is not known to be 0, and Default(): bool is not known to be false. It exists purely so that the library can say "the padding value" — the value stored in a Vec beyond its length, or in a Map outside its domain — without committing to anything.

procedure DefaultIsAFunction()

{

  assert Default(): int == Default(): int;

}

 

procedure DefaultIsUnknown()

{

  assert Default(): int == 0;

}

 

procedure DefaultBool()

{

  assert Default(): bool == false;

}

boogie /lib:base default.bpl

default.bpl(8,3): Error: this assertion could not be proved

Execution trace:

    default.bpl(8,3): anon0

default.bpl(13,3): Error: this assertion could not be proved

Execution trace:

    default.bpl(13,3): anon0

 

Boogie program verifier finished with 1 verified, 2 errors

Do not assume anything about Default(); and do not add an axiom fixing it, because a single Default is shared by every use at that type.

11.4 Option, Unit and UnitMap🔗

datatype Option<T> { None(), Some(t: T) }

 

datatype Unit { Unit() }

 

type UnitMap K = Map K Unit;

Option is the usual two-constructor option type; the payload accessor is named t, so it is o->t and not o->val. Unit is the one-element type, and UnitMap K is the type synonym for a finite map with Unit values, i.e. a finite set in the Map representation. In Civl code UnitMap K is the standard type of a pool of linear resources.

procedure Options()

{

  var o: Option int;

 

  o := None();

  assert o is None;

  o := Some(4);

  assert o is Some && o->t == 4;

  assert None(): Option int != Some(0);

}

 

procedure Units()

{

  var u: Unit;

  var m: UnitMap int;

 

  assert u == Unit();

  m := Map_Empty();

  m := Map_Update(m, 1, Unit());

  assert Map_Contains(m, 1);

}

boogie /lib:base options.bpl

 

Boogie program verifier finished with 2 verified, 0 errors

11.5 Sets🔗

Sets are [T]bool maps; the Set_* functions are all {:inline} wrappers around map combinators and map select/update, so they carry no axioms of their own and cost nothing.

function {:inline} Set_Empty<T>(): [T]bool        { MapConst(false) }

function {:inline} Set_Contains<T>(a: [T]bool, t: T): bool  { a[t] }

function {:inline} Set_IsSubset<T>(a: [T]bool, b: [T]bool): bool

                                                  { MapImp(a, b) == MapConst(true) }

function {:inline} Set_IsDisjoint<T>(a: [T]bool, b: [T]bool): bool

                                                  { Set_Intersection(a, b) == Set_Empty() }

function {:inline} Set_Add<T>(a: [T]bool, t: T): [T]bool    { a[t := true] }

function {:inline} Set_Singleton<T>(t: T): [T]bool          { Set_Add(Set_Empty(), t) }

function {:inline} Set_Remove<T>(a: [T]bool, t: T): [T]bool { a[t := false] }

function {:inline} Set_Union<T>(a: [T]bool, b: [T]bool): [T]bool         { MapOr(a, b) }

function {:inline} Set_Difference<T>(a: [T]bool, b: [T]bool): [T]bool    { MapDiff(a, b) }

function {:inline} Set_Intersection<T>(a: [T]bool, b: [T]bool): [T]bool  { MapAnd(a, b) }

(The bodies above are reformatted onto one line each; the declarations are otherwise verbatim.)

There is also a choice function, the only part of the set layer with an axiom:

function Choice<T>(a: [T]bool): T;

axiom (forall<T> a: [T]bool :: {Choice(a)} a == MapConst(false) || a[Choice(a)]);

Choice(a) is some member of a whenever a is non-empty, and completely unconstrained when a is empty. It is deterministic — the same set always yields the same element — but nothing relates Choice of one set to Choice of another.

procedure SetOps()

{

  var a, b: [int]bool;

 

  a := Set_Empty();

  assert !Set_Contains(a, 3);

  a := Set_Add(a, 3);

  a := Set_Add(a, 5);

  assert Set_Contains(a, 5);

  b := Set_Singleton(5);

  assert Set_IsSubset(b, a);

  assert !Set_IsSubset(a, b);

  assert Set_IsDisjoint(Set_Singleton(1), Set_Singleton(2));

  assert Set_Difference(a, b) == Set_Singleton(3);

  assert Set_Union(b, Set_Singleton(3)) == a;

  assert Set_Intersection(a, b) == b;

  assert Set_Remove(a, 5) == Set_Singleton(3);

}

 

procedure ChoiceFn(a: [int]bool)

requires Set_Contains(a, 42);

{

  assert Set_Contains(a, Choice(a));

  assert Choice(Set_Singleton(7)) == 7;

}

boogie /lib:base sets.bpl

 

Boogie program verifier finished with 2 verified, 0 errors

11.5.1 Set cardinality: /lib:set_size🔗

set_size.bpl adds an uninterpreted cardinality function with six axioms and three lemmas. It requires /lib:base.

function Set_Size<T>(a: [T]bool) : int;

 

axiom (forall<T> a: [T]bool :: 0 <= Set_Size(a));

 

axiom (forall<T> :: Set_Size(Set_Empty(): [T]bool) == 0);

 

axiom (forall<T> a: [T]bool, t: T :: {Set_Add(a, t)} Set_Size(Set_Add(a, t)) == if Set_Contains(a, t) then Set_Size(a) else Set_Size(a) + 1);

 

axiom (forall<T> a: [T]bool, t: T :: {Set_Remove(a, t)} Set_Size(Set_Remove(a, t)) == if Set_Contains(a, t) then Set_Size(a) - 1 else Set_Size(a));

 

axiom (forall<T> a: [T]bool, b: [T]bool :: {Set_Size(Set_Difference(a, b))} {Set_Size(Set_Intersection(a, b))}

        Set_Size(a) == Set_Size(Set_Difference(a, b)) + Set_Size(Set_Intersection(a, b)));

 

axiom (forall<T> a: [T]bool, b: [T]bool :: {Set_Size(Set_Union(a, b))} {Set_Size(Set_Intersection(a, b))}

        Set_Size(Set_Union(a, b)) + Set_Size(Set_Intersection(a, b)) == Set_Size(a) + Set_Size(b));

Note what is not there. Set_Size is non-negative, correct on the empty set, and correct under single-element add/remove and under the inclusion-exclusion identities. There is no axiom saying that a non-empty set has positive size, and no axiom relating subset to size. Note also that the last four axioms are trigger-guarded on Set_Add, Set_Remove, Set_Size(Set_Difference(...)), Set_Size(Set_Intersection(...)) and Set_Size(Set_Union(...)): if none of those terms occurs in your program, they are never instantiated. The subset fact is supplied as a lemma instead:

pure procedure Lemma_SetSize_Add<T>(a: [T]bool, t: T) returns (b: [T]bool);

requires !Set_Contains(a, t);

ensures b == Set_Add(a, t);

ensures Set_Size(b) == Set_Size(a) + 1;

 

pure procedure Lemma_SetSize_Remove<T>(a: [T]bool, t: T) returns (b: [T]bool);

requires Set_Contains(a, t);

ensures b == Set_Remove(a, t);

ensures Set_Size(b) + 1 == Set_Size(a);

 

pure procedure Lemma_SetSize_Subset<T>(a: [T]bool, b: [T]bool);

requires Set_IsSubset(a, b);

ensures a == b || Set_Size(a) < Set_Size(b);

These are pure procedure declarations with no body. A body-less procedure is trusted: its postcondition is assumed at every call site and never discharged. The lemmas are all sound — Lemma_SetSize_Subset, the interesting one, does follow from the six axioms — but only through a witness element that no trigger produces. Handed a witness explicitly, the prover gets there:

// Given a witness element the strict inequality does follow from the axioms.

procedure StrictFromWitness(a: [int]bool, b: [int]bool, t: int)

requires Set_IsSubset(a, b);

requires Set_Contains(b, t) && !Set_Contains(a, t);

{

  assert Set_Size(Set_Intersection(b, a)) == Set_Size(a);

  assert Set_Size(Set_Remove(Set_Difference(b, a), t)) >= 0;

  assert Set_Size(a) < Set_Size(b);

}

 

// And a witness always exists when a is a proper subset of b.

procedure WitnessExists(a: [int]bool, b: [int]bool)

requires Set_IsSubset(a, b);

requires a != b;

{

  assert (exists t: int :: Set_Contains(b, t) && !Set_Contains(a, t));

}

boogie /lib:base /lib:set_size setsize-derive.bpl

 

Boogie program verifier finished with 2 verified, 0 errors

The second assert in StrictFromWitness is the whole trick: it puts the term Set_Remove(Set_Difference(b, a), t) in front of the prover, which fires the Set_Remove axiom and, with non-negativity, yields Set_Size(Set_Difference(b, a)) >= 1. Nothing in the axiom set makes that term appear on its own, which is why the lemma exists.

The pure qualifier comes from the grammar,

Pure<ref bool isPure>

= ["pure" (. isPure = true; .)]

  .

and may prefix either a procedure or an action. A pure procedure has no state effects and may be called from ordinary procedures, which is what makes it a convenient lemma vehicle.

procedure Sizes()

{

  var a, b: [int]bool;

 

  a := Set_Empty();

  assert Set_Size(a) == 0;

  a := Set_Add(a, 3);

  assert Set_Size(a) == 1;

  a := Set_Add(a, 3);

  assert Set_Size(a) == 1;

  b := Set_Add(a, 5);

  assert Set_Size(b) == 2;

  assert Set_Size(Set_Remove(b, 5)) == 1;

}

 

procedure Monotone(a: [int]bool, b: [int]bool)

requires Set_IsSubset(a, b);

requires a != b;

{

  call Lemma_SetSize_Subset(a, b);

  assert Set_Size(a) < Set_Size(b);

}

 

// Nothing fires the difference/intersection axiom here, so not even the

// non-strict inequality comes out.

procedure NonStrict(a: [int]bool, b: [int]bool)

requires Set_IsSubset(a, b);

{

  assert Set_Size(a) <= Set_Size(b);

}

 

// Mentioning a trigger term is enough for the non-strict inequality.

procedure NonStrictTriggered(a: [int]bool, b: [int]bool)

requires Set_IsSubset(a, b);

{

  assert Set_Size(Set_Intersection(b, a)) == Set_Size(a);

  assert Set_Size(a) <= Set_Size(b);

}

 

// The strict inequality still does not come out: nothing puts a term in

// front of the prover that would give a non-empty set a positive size.

procedure StrictWithoutLemma(a: [int]bool, b: [int]bool)

requires Set_IsSubset(a, b);

requires a != b;

{

  assert Set_Size(Set_Intersection(b, a)) == Set_Size(a);

  assert Set_Size(a) < Set_Size(b);

}

boogie /lib:base /lib:set_size setsize.bpl

setsize.bpl(29,3): Error: this assertion could not be proved

Execution trace:

    setsize.bpl(29,3): anon0

setsize.bpl(47,3): Error: this assertion could not be proved

Execution trace:

    setsize.bpl(46,3): anon0

 

Boogie program verifier finished with 3 verified, 2 errors

11.6 Vectors🔗

Vec is the library’s array/list type. It is the part of the library most likely to be reached for by non-Civl users.

11.6.1 Representation🔗

datatype Vec<T> { Vec(contents: [int]T, len: int) }

A vector is a pair of an infinite integer-indexed map and a length. The elements are contents[0] through contents[len-1]. Vec is an ordinary Boogie datatype, so Vec(m, n) is a legal expression for any map m and any integer n, and v->contents and v->len are legal field accesses.

11.6.2 The canonicalisation axioms🔗

axiom {:ctor "Vec"} (forall<T> x: Vec T :: {x->len}{x->contents} MapIte(Range(0, x->len), MapConst(Default()), x->contents) == MapConst(Default()));

axiom {:ctor "Vec"} (forall<T> x: Vec T :: {x->len} x->len >= 0);

Unpacked, the first axiom says: overwriting the live range [0, len) with Default() leaves a map that is Default() everywhere. That is, for every index i outside [0, len), contents[i] == Default(). The second says lengths are non-negative.

These are the axioms that make vectors behave. They give you, for free:

procedure OutOfRange(v: Vec int)

{

  assert Vec_Nth(v, -1) == Default();

  assert Vec_Nth(v, Vec_Len(v)) == Default();

  assert Vec_Len(v) >= 0;

}

 

procedure EmptyIsUnique(v: Vec int)

requires Vec_Len(v) == 0;

{

  assert v == Vec_Empty();

}

 

procedure Degenerate(v: Vec int, i: int, j: int)

requires !(0 <= i && i < Vec_Len(v) && 0 <= j && j < Vec_Len(v));

{

  assert Vec_Swap(v, i, j) == v;

}

 

procedure RemoveEmpty(v: Vec int)

requires Vec_Len(v) == 0;

{

  assert Vec_Remove(v) == v;

}

 

procedure SliceDegenerate(v: Vec int, i: int, j: int)

requires !(0 <= i && i < j && j <= Vec_Len(v));

{

  assert Vec_Slice(v, i, j) == Vec_Empty();

}

boogie /lib:base vec-canonical.bpl

 

Boogie program verifier finished with 5 verified, 0 errors

They also give vectors extensionality: two vectors with the same length whose in-range elements agree are equal, because their contents maps agree everywhere.

Vectors are built with Vec_Empty, Vec_Append, Vec_Update, Vec_Concat, Vec_Slice, Vec_Swap and Vec_Remove, all of which maintain the representation these axioms describe. If you need an operation the library does not have, define it in terms of those. Reading v->contents and v->len directly is fine.

The {:ctor "Vec"} attribute on both axioms is dead. It was read by an earlier version of the monomorphiser and the code that read it was deleted in commit 76b6a373; no C# in the current tree looks at "ctor". The same vestigial attribute appears on every axiom in node.bpl.

11.6.3 Vector operations🔗

function {:inline} Vec_Empty<T>(): Vec T

{

  Vec(MapConst(Default()), 0)

}

function {:inline} Vec_Append<T>(v: Vec T, x: T) : Vec T

{

  Vec(v->contents[v->len := x], v->len + 1)

}

function {:inline} Vec_Update<T>(v: Vec T, i: int, x: T) : Vec T

{

  if (0 <= i && i < v->len) then Vec(v->contents[i := x], v->len) else v

}

function {:inline} Vec_Nth<T>(v: Vec T, i: int): T

{

  v->contents[i]

}

function {:inline} Vec_Len<T>(v: Vec T): int

{

  v->len

}

function {:inline} Vec_Contains<T>(v: Vec T, i: int): bool

{

  0 <= i && i < Vec_Len(v)

}

(Regrouped: in base.bpl Vec_Concat and Vec_Slice sit between Vec_Len and Vec_Swap, and Vec_Contains comes last of all. The declarations themselves are verbatim.) Every one of them is {:inline}, so they disappear before the VC is built and cost nothing at the prover.

function {:inline} Vec_Swap<T>(v: Vec T, i: int, j: int): Vec T

{

  (

    var cond := 0 <= i && i < v->len && 0 <= j && j < v->len;

    Vec(v->contents[i := v->contents[if (cond) then j else i]][j := v->contents[if (cond) then i else j]], v->len)

  )

}

 

function {:inline} Vec_Remove<T>(v: Vec T): Vec T

{

  (

    var cond, new_len := 0 < v->len, v->len - 1;

    Vec(v->contents[new_len := if (cond) then Default() else v->contents[new_len]], if (cond) then new_len else v->len)

  )

}

Both are written so that the degenerate case reduces to the identity while staying canonical — this is why Vec_Remove writes Default() into the vacated slot, and why the cond guard is pushed inside the map update rather than wrapped around the whole Vec(...) term.

procedure Build()

{

  var v: Vec int;

 

  v := Vec_Empty();

  assert Vec_Len(v) == 0;

  v := Vec_Append(v, 10);

  v := Vec_Append(v, 20);

  v := Vec_Append(v, 30);

  assert Vec_Len(v) == 3;

  assert Vec_Nth(v, 0) == 10;

  assert Vec_Nth(v, 2) == 30;

  assert Vec_Contains(v, 2);

  assert !Vec_Contains(v, 3);

  v := Vec_Update(v, 1, 99);

  assert Vec_Nth(v, 1) == 99 && Vec_Len(v) == 3;

  v := Vec_Update(v, 7, 0);

  assert Vec_Len(v) == 3 && Vec_Nth(v, 1) == 99;

  v := Vec_Remove(v);

  assert Vec_Len(v) == 2;

  v := Vec_Swap(v, 0, 1);

  assert Vec_Nth(v, 0) == 99 && Vec_Nth(v, 1) == 10;

}

boogie /lib:base vec-basics.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

11.6.4 Concat and Slice🔗

function {:inline} Vec_Concat<T>(v1: Vec T, v2: Vec T): Vec T

{

  Vec(

    (lambda {:pool "Concat"} i: int ::

      if (i < 0) then Default()

      else if (0 <= i && i < Vec_Len(v1)) then Vec_Nth(v1, i)

      else if (Vec_Len(v1) <= i && i < Vec_Len(v1) + Vec_Len(v2)) then Vec_Nth(v2, i - Vec_Len(v1))

      else Default()),

    Vec_Len(v1) + Vec_Len(v2)

  )

}

 

function {:inline} Vec_Slice<T>(v: Vec T, i: int, j: int): Vec T

{

  (

    var cond := 0 <= i && i < j && j <= v->len;

    Vec(

      (lambda {:pool "Slice"} k: int :: if (cond && 0 <= k && k < j - i) then Vec_Nth(v, k + i) else Default()),

      if (cond) then j - i else 0

    )

  )

}

Vec_Concat(v1, v2) is the concatenation. Vec_Slice(v, i, j) is the half-open slice [i, j), and yields Vec_Empty() whenever the range is degenerate (i < 0, i >= j, or j > Vec_Len(v)) — again a total function, not a partial one.

Both build their contents with a lambda rather than a chain of updates, and both tag the lambda with {:pool "Concat"} / {:pool "Slice"}. Those names are instantiation pools: Boogie’s lambda-instantiation machinery will only instantiate the lambda at index terms that have been added to the pool. Simple shape facts come out without help:

type Element;

 

procedure SplitJoin(A: Vec Element, i: int)

requires 0 <= i && i < Vec_Len(A);

{

  assert Vec_Concat(Vec_Slice(A, 0, i), Vec_Slice(A, i, Vec_Len(A))) == A;

}

 

procedure SliceShape(A: Vec Element, i: int, j: int)

requires 0 <= i && i < j && j <= Vec_Len(A);

{

  assert Vec_Len(Vec_Slice(A, i, j)) == j - i;

  assert Vec_Nth(Vec_Slice(A, i, j), 0) == Vec_Nth(A, i);

  assert Vec_Len(Vec_Slice(A, 5, 5)) == 0;

}

 

procedure ConcatShape(A: Vec Element, B: Vec Element)

{

  assert Vec_Len(Vec_Concat(A, B)) == Vec_Len(A) + Vec_Len(B);

}

boogie /lib:base vec-slice.bpl

 

Boogie program verifier finished with 3 verified, 0 errors

Harder equalities between slice/concat terms usually do not, and need indices fed into the pool with {:add_to_pool "Slice", e} on an assert or assume — Boogie’s own instantiation engine, described in Pool-based quantifier instantiation, rather than a solver trigger. The idiom, taken from Test/inst/vector.bpl, is covered next.

11.6.5 Extensionality: Vec_Ext🔗

// extensionality lemma to be used explicitly by the programmer

procedure Vec_Ext<T>(A: Vec T, B: Vec T) returns (i: int);

ensures A == B || Vec_Len(A) != Vec_Len(B) || Vec_Nth(A, i) != Vec_Nth(B, i);

A body-less — hence trusted — procedure that hands you a witness index: if A and B are different but the same length, then they differ at the returned index i. Note it is a plain procedure, not pure, so it can only be called from a procedure or implementation body, and it must be called; there is no function form.

You do not need it for the elementwise-equality-implies-equality direction — the canonicalisation axiom plus map extensionality already give that. You need it when the two vectors are Concat/Slice terms, where the prover cannot compare the underlying lambdas without being handed an index to instantiate them at. The returned i is precisely what you then push into the pool:

type Element;

 

procedure WithoutExt(A: Vec Element, B: Vec Element, i: int, e: Element)

requires 0 <= i && i < Vec_Len(A);

requires Vec_Len(A) == Vec_Len(B);

requires Vec_Nth(A, i) == Vec_Nth(B, Vec_Len(B) - 1);

requires Vec_Concat(Vec_Slice(A, 0, i), Vec_Slice(A, i + 1, Vec_Len(A))) == Vec_Slice(B, 0, Vec_Len(B) - 1);

{

  var A', B': Vec Element;

 

  A' := Vec_Append(A, e);

  B' := Vec_Swap(Vec_Append(B, e), Vec_Len(B) - 1, Vec_Len(B));

 

  assert Vec_Concat(Vec_Slice(A', 0, i), Vec_Slice(A', i + 1, Vec_Len(A')))

      == Vec_Slice(B', 0, Vec_Len(B') - 1);

}

 

procedure WithExt(A: Vec Element, B: Vec Element, i: int, e: Element)

requires 0 <= i && i < Vec_Len(A);

requires Vec_Len(A) == Vec_Len(B);

requires Vec_Nth(A, i) == Vec_Nth(B, Vec_Len(B) - 1);

requires Vec_Concat(Vec_Slice(A, 0, i), Vec_Slice(A, i + 1, Vec_Len(A))) == Vec_Slice(B, 0, Vec_Len(B) - 1);

{

  var A', B': Vec Element;

  var x: int;

 

  A' := Vec_Append(A, e);

  B' := Vec_Swap(Vec_Append(B, e), Vec_Len(B) - 1, Vec_Len(B));

 

  call x := Vec_Ext(Vec_Concat(Vec_Slice(A', 0, i), Vec_Slice(A', i + 1, Vec_Len(A'))),

                    Vec_Slice(B', 0, Vec_Len(B') - 1));

  assert {:add_to_pool "Slice", x}

         Vec_Concat(Vec_Slice(A', 0, i), Vec_Slice(A', i + 1, Vec_Len(A')))

      == Vec_Slice(B', 0, Vec_Len(B') - 1);

}

boogie /lib:base vec-ext.bpl

vec-ext.bpl(14,3): Error: this assertion could not be proved

Execution trace:

    vec-ext.bpl(11,6): anon0

 

Boogie program verifier finished with 1 verified, 1 error

The two procedures are identical apart from the Vec_Ext call and the pool annotation. In real proofs you often need several offsets of the witness — Test/inst/vector.bpl contains lines such as assert {:add_to_pool "Slice", 0, x + j, x - j, x, x + 1, x - 1} — which is a fair indication of how much manual steering vector proofs require.

11.7 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;

function {:builtin "seq.++"} Seq_Concat<T>(a: Seq T, b: Seq T): Seq T;

function {:builtin "seq.unit"} Seq_Unit<T>(v: T): Seq T;

function {:builtin "seq.nth"} Seq_Nth<T>(a: Seq T, i: int): T;

function {:builtin "seq.extract"} Seq_Extract<T>(a: Seq T, pos: int, length: int): Seq T;

An alternative to Vec that hands the work to the solver’s own sequence theory instead of axiomatising it in Boogie. Seq T maps onto Z3’s Seq sort and the six functions onto seq.empty, seq.len, seq.++, seq.unit, seq.nth and seq.extract. These are not part of the SMT-LIB standard, so a program using Seq is tied to a solver that implements the sequence theory.

procedure SeqBasics()

{

  var s: Seq int;

 

  s := Seq_Concat(Seq_Unit(1), Seq_Unit(2));

  assert Seq_Len(s) == 2;

  assert Seq_Nth(s, 0) == 1;

  assert Seq_Nth(s, 1) == 2;

  assert Seq_Len(Seq_Empty(): Seq int) == 0;

  assert Seq_Extract(s, 1, 1) == Seq_Unit(2);

}

boogie /lib:base seq.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

Trade-offs against Vec: sequences are decided (incompletely) by the solver and need no manual pool steering, but out-of-range Seq_Nth is unspecified rather than Default(), and there is no Seq analogue of the canonicalisation axioms. There are no library functions to convert between Vec and Seq. Test/sequences/ holds two small programs, each in a version that declares the {:builtin} sequence functions by hand at a fixed element type (intseq.bpl, intseq_datatype.bpl) and a version that gets the polymorphic ones from /lib:base (intseq_lib.bpl, intseq_datatype_lib.bpl). There is no Vec version there.

11.8 Finite maps🔗

datatype Map<T,U> { Map(dom: [T]bool, val: [T]U) }

A finite map is a domain set plus a total value map. It has the same shape of representation invariant as Vec — val is meant to be Default() outside dom — but, crucially, there is no axiom enforcing it. The invariant is exposed as a predicate you assume where you need it:

function {:inline} Map_WellFormed<T,U>(a: Map T U): bool

{

  a->val == MapIte(a->dom, a->val, MapConst(Default()))

}

Constructing a non-well-formed Map is legal; you simply lose extensionality until you assume well-formedness:

// Map is a free datatype: nothing forces val to be Default() outside dom.

procedure NotWellFormed(a: Map int int, b: Map int int)

requires a->dom == b->dom;

requires (forall t: int :: Set_Contains(a->dom, t) ==> Map_At(a, t) == Map_At(b, t));

{

  assert a == b;

}

 

procedure WellFormed(a: Map int int, b: Map int int)

requires Map_WellFormed(a) && Map_WellFormed(b);

requires a->dom == b->dom;

requires (forall t: int :: Set_Contains(a->dom, t) ==> Map_At(a, t) == Map_At(b, t));

{

  assert a == b;

}

boogie /lib:base fmap-wf.bpl

fmap-wf.bpl(6,3): Error: this assertion could not be proved

Execution trace:

    fmap-wf.bpl(6,3): anon0

 

Boogie program verifier finished with 1 verified, 1 error

11.8.1 Operations🔗

function {:inline} Map_Empty<T,U>(): Map T U

{

  Map(MapConst(false), MapConst(Default()))

}

function {:inline} Map_Singleton<T,U>(t: T, u: U): Map T U

{

  Map_Update(Map_Empty(), t, u)

}

function {:inline} Map_Contains<T,U>(a: Map T U, t: T): bool

{

  Set_Contains(a->dom, t)

}

function {:inline} Map_IsDisjoint<T,U>(a: Map T U, b: Map T U): bool

{

  Set_IsDisjoint(a->dom, b->dom)

}

function {:inline} Map_At<T,U>(a: Map T U, t: T): U

{

  a->val[t]

}

function {:inline} Map_Remove<T,U>(a: Map T U, t: T): Map T U

{

  Map(Set_Remove(a->dom, t), a->val[t := Default()])

}

function {:inline} Map_Update<T,U>(a: Map T U, t: T, u: U): Map T U

{

  Map(Set_Add(a->dom, t), a->val[t := u])

}

function {:inline} Map_Swap<T,U>(a: Map T U, t1: T, t2: T): Map T U

{

  (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))

}

function {:inline} Map_Extract<T,U>(a: Map T U, t: [T]bool): Map T U

{

  Map(t, MapIte(t, a->val, MapConst(Default())))

}

function {:inline} Map_Exclude<T,U>(a: Map T U, t: [T]bool): Map T U

{

  Map(Set_Difference(a->dom, t), MapIte(t, MapConst(Default()), a->val))

}

function {:inline} Map_Union<T,U>(a: Map T U, b: Map T U): Map T U

{

  Map(Set_Union(a->dom, b->dom), MapIte(a->dom, a->val, b->val))

}

Points worth noting:

procedure MapOps()

{

  var m: Map int bool;

 

  m := Map_Empty();

  assert !Map_Contains(m, 1);

  assert Map_WellFormed(m);

  m := Map_Update(m, 1, true);

  m := Map_Update(m, 2, false);

  assert Map_Contains(m, 2);

  assert Map_At(m, 1) == true;

  assert Map_Collector(m) == Set_Add(Set_Singleton(1), 2);

  assert Map_Remove(m, 1) == Map_Singleton(2, false);

  assert Map_IsDisjoint(Map_Singleton(9, true), m);

  assert Map_Extract(m, Set_Singleton(1)) == Map_Singleton(1, true);

  assert Map_Exclude(m, Set_Singleton(1)) == Map_Singleton(2, false);

  assert Map_Union(Map_Singleton(1, true), Map_Singleton(2, false)) == m;

  assert Map_Swap(m, 1, 2) == Map_Update(Map_Update(m, 1, false), 2, true);

}

boogie /lib:base fmap.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

11.8.2 Permission collectors🔗

function {:inline} Map_Collector<T,U>(a: Map T U): [T]bool

{

  a->dom

}

 

function {:inline} Map_Collector_Empty<T,U,P>(a: Map T U): [P]bool

{

  MapConst(false)

}

These two are not really for user code; the Civl linear type checker instantiates them by name to compute the permission set of a linear Map variable. Map_Collector is used when the permission type is the map’s key type; Map_Collector_Empty is used for every other permission type, which is the implementation’s way of saying that permissions held inside a map’s values are not tracked ("permission collection for values stored in Map is unbounded and is not being done"). One_Collector below plays the same role for One.

11.9 Civl-oriented types and primitives🔗

The tail of base.bpl exists to support Civl’s linear type system. These declarations are usable in ordinary Boogie programs too — One, Cell and Tag are ordinary datatypes and Loc an ordinary uninterpreted type — but the primitives only acquire their meaning through a rewriting pass, described below.

11.9.1 One, Cell, Tag, Loc🔗

/// singleton set

datatype One<T> { One(val: T) }

 

function {:inline} One_Collector<T>(a: One T): [One T]bool

{

  Set_Singleton(a)

}

 

/// singleton map

datatype Cell<T,U> { Cell(key: One T, val: U) }

 

type Loc;

 

datatype Tag<V> { Tag(loc: Loc, val: V) }

 

function {:inline} Tags<V>(loc: Loc, xs:[V]bool): [One (Tag V)]bool {

    (lambda x: One (Tag V):: x->val->loc == loc && Set_Contains(xs, x->val->val))

}

11.9.2 The linear primitives🔗

/// linear primitives

pure procedure Move<T>({:linear_in} u: T, {:linear_out} v: T);

pure procedure {:inline 1} Map_MakeEmpty<K,V>() returns ({:linear} m: Map K V)

{

  m := Map_Empty();

}

pure procedure One_Get<K>({:linear} path: UnitMap K, {:linear_out} l: K);

pure procedure One_Put<K>({:linear} path: UnitMap K, {:linear_in} l: K);

pure procedure Map_Get<K,V>({:linear} path: Map K V, {:linear_out} k: K) returns ({:linear} v: V);

pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} k: K, {:linear_in} v: V);

pure procedure Map_Split<K,V>({:linear} path: Map K V, k: [K]bool) returns ({:linear} l: Map K V);

pure procedure Map_Join<K,V>({:linear} path: Map K V, {:linear_in} l: Map K V);

pure procedure Path_Load<V>(path: V) returns (v: V);

pure procedure Path_Store<V>(path: V, v: V);

These ten names (together with Loc_New, Tag_New and Tags_New below) are hard-coded in the C# as CivlPrimitives.LinearPrimitives. Their declarations are almost empty: the real semantics is that LinearRewriter replaces each call to one of them with a short sequence of assert and assignment commands. The rewriting is applied to every implementation whose procedure is not a yield procedure — so action bodies, pure procedure bodies and ordinary procedure bodies all work.

The first argument of One_Get, One_Put, Map_Get, Map_Put, Map_Split, Map_Join, Path_Load and Path_Store is a path expression: a variable, optionally followed by field accesses and map indexings. It is assigned through, so it must be assignable. Passing a procedure’s own in-parameter is rejected:

type Res;

 

// The path argument is assigned through, so it must be assignable.

pure procedure Take({:linear} path: Map (One Res) int, {:linear_out} k: One Res)

  returns ({:linear} v: int)

{

  call v := Map_Get(path, k);

}

boogie /lib:base lin-path-illegal.bpl

lin-path-illegal.bpl(7,2): Error: primitive assigns to input variable: path

1 type checking errors detected in lin-path-illegal.bpl

A path may also not go through the val field of a One, nor through the dom field of a Map:

type Res;

 

procedure ThroughDom({:linear_in} p: UnitMap (One Res), a: One Res)

{

  var {:linear} pool: UnitMap (One Res);

  var b: bool;

  pool := p;

  call b := Path_Load(pool->dom[a]);

}

boogie /lib:base lin-path-illegal2.bpl

lin-path-illegal2.bpl(8,2): Error: illegal path expression at position 0

1 type checking errors detected in lin-path-illegal2.bpl

Every step of a legal path is checked at verification time: indexing the val field of a Map generates "map lookup failed" (the assertion is Map_Contains of the index) and projecting a multi-constructor datatype generates "field lookup failed" (a disjunction of is-tests over the constructors that have the field).

The rewritings, verbatim from LinearRewriter:

Map_MakeEmpty has no rewriting: like Loc_New, Tag_New and Tags_New it is {:inline 1} with a real body, and LinearRewriter passes the call through untouched. Those four are still primitives — they are in CivlPrimitives.LinearPrimitives, so the linear type checker treats their arguments specially — they just have nothing to rewrite to.

type Res;

 

procedure Demo({:linear_in} r: One Res)

{

  var {:linear} m: Map (One Res) int;

  var {:linear} r': One Res;

  var v: int;

 

  r' := r;

  call m := Map_MakeEmpty();

  call Map_Put(m, r', 42);

  assert Map_Contains(m, r');

  call v := Map_Get(m, r');

  assert v == 42;

  assert !Map_Contains(m, r');

}

boogie /lib:base lin-map.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

Note the direction of the linear annotations on Map_Get: the key is {:linear_out} (ownership of the key comes back to the caller) and the returned value is {:linear}. Getting this backwards produces a type error about out-parameter 0.

When the check fails you get the primitive’s own message, and the inlined library body appears in the trace:

type Res;

 

procedure Demo({:linear_in} r: One Res)

{

  var {:linear} m: Map (One Res) int;

  var {:linear} r': One Res;

  var v: int;

 

  r' := r;

  call m := Map_MakeEmpty();

  call v := Map_Get(m, r');      // m is empty

}

boogie /lib:base lin-get-fail.bpl

lin-get-fail.bpl(11,3): Error: Map_Get failed

Execution trace:

    lin-get-fail.bpl(9,6): anon0

    base.bpl(277,5): inline$Map_MakeEmpty_2739_23$0$anon0

    lin-get-fail.bpl(9,6): anon0$1

 

Boogie program verifier finished with 0 verified, 1 error

The pool operations, on a UnitMap:

type Res;

 

procedure Pool({:linear_in} p: UnitMap (One Res), a: One Res, b: One Res)

requires Map_Contains(p, a);

{

  var {:linear} pool: UnitMap (One Res);

  var {:linear} half: UnitMap (One Res);

  var {:linear} x: One Res;

 

  pool := p;

 

  call One_Get(pool, a);

  assert !Map_Contains(pool, a);

  x := a;

 

  call One_Put(pool, x);

  assert Map_Contains(pool, a);

 

  call half := Map_Split(pool, Set_Singleton(a));

  assert Map_Contains(half, a) && !Map_Contains(pool, a);

  call Map_Join(pool, half);

  assert Map_Contains(pool, a);

}

boogie /lib:base lin-pool.bpl

 

Boogie program verifier finished with 1 verified, 0 errors

type Res;

 

procedure GetMissing({:linear_in} p: UnitMap (One Res), a: One Res)

{

  var {:linear} pool: UnitMap (One Res);

  pool := p;

  call One_Get(pool, a);

}

 

procedure SplitTooMuch({:linear_in} p: UnitMap (One Res), s: [One Res]bool)

{

  var {:linear} pool: UnitMap (One Res);

  var {:linear} half: UnitMap (One Res);

  pool := p;

  call half := Map_Split(pool, s);

}

boogie /lib:base lin-fail.bpl

lin-fail.bpl(7,3): Error: One_Get failed

Execution trace:

    lin-fail.bpl(6,8): anon0

lin-fail.bpl(15,3): Error: Map_Split failed

Execution trace:

    lin-fail.bpl(14,8): anon0

 

Boogie program verifier finished with 0 verified, 2 errors

And a two-step path through a Map of Cells, showing both the successful load/store and the path check:

type Res;

 

procedure Paths({:linear_in} p: Map (One Res) (Cell Res int), a: One Res)

requires Map_Contains(p, a);

{

  var {:linear} m: Map (One Res) (Cell Res int);

  var v: int;

 

  m := p;

  call v := Path_Load(m->val[a]->val);

  call Path_Store(m->val[a]->val, v + 1);

  call v := Path_Load(m->val[a]->val);

  assert v == Map_At(p, a)->val + 1;

}

 

procedure BadPath({:linear_in} p: Map (One Res) (Cell Res int), a: One Res)

{

  var {:linear} m: Map (One Res) (Cell Res int);

  var v: int;

 

  m := p;

  call v := Path_Load(m->val[a]->val);   // a may not be in m

}

boogie /lib:base lin-path.bpl

lin-path.bpl(22,29): Error: map lookup failed

Execution trace:

    lin-path.bpl(21,5): anon0

 

Boogie program verifier finished with 1 verified, 1 error

11.9.3 Surprise: Map_Put assumes freshness of a linear key🔗

The assume !Map_Contains(path, k) inserted by Map_Put for a linear key is not visible anywhere in base.bpl, and it is not an assertion — it is a free assumption. It is justified by the linear discipline (if you own the key, nobody else can, so it cannot already be in the map), but it means Map_Put can silently teach the prover a fact about the pre-state:

type Res;

 

// Map_Put with a linear key ASSUMES the key was not already in the map.

procedure PutLinearKey({:linear_in} p: Map (One Res) int, {:linear_in} r: One Res)

{

  var {:linear} m: Map (One Res) int;

  var {:linear} r': One Res;

 

  m := p;

  r' := r;

  call Map_Put(m, r', 1);

  assert !Map_Contains(p, r);

}

 

// With an ordinary key type no such assumption is made.

procedure PutOrdinaryKey({:linear_in} p: Map int int, k: int)

{

  var {:linear} m: Map int int;

 

  m := p;

  call Map_Put(m, k, 1);

  assert !Map_Contains(p, k);

}

boogie /lib:base lin-put-fresh.bpl

lin-put-fresh.bpl(22,3): Error: this assertion could not be proved

Execution trace:

    lin-put-fresh.bpl(20,5): anon0

 

Boogie program verifier finished with 1 verified, 1 error

The first procedure verifies. This is the mechanism that makes allocation work (see the next subsection), but it is worth knowing that it exists.

11.9.4 Allocation: Loc_New, Tag_New, Tags_New🔗

pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One Loc)

{

  assume {:add_to_pool "Loc_New", l} true;

}

 

pure procedure {:inline 1} Tag_New() returns ({:linear} {:pool "Loc_New"} l: One Loc, {:linear} tag: One (Tag Unit))

{

  assume {:add_to_pool "Loc_New", l} true;

  tag := One(Tag(l->val, Unit()));

}

 

pure procedure {:inline 1} Tags_New<V>(vals: [V]bool) returns ({:linear} {:pool "Loc_New"} l: One Loc, {:linear} tags: UnitMap (One (Tag V)))

{

  assume {:add_to_pool "Loc_New", l} true;

  tags := Map(Tags(l->val, vals), MapConst(Unit()));

}

These bodies contain no freshness assumption of any kind. The assume ... true is a no-op whose only purpose is the {:add_to_pool} annotation, which registers the new location in the "Loc_New" instantiation pool. Two calls to Loc_New therefore do not give you two distinct locations:

procedure Fresh()

{

  var {:linear} l1: One Loc;

  var {:linear} l2: One Loc;

 

  call l1 := Loc_New();

  call l2 := Loc_New();

  assert l1 != l2;

}

 

procedure Tagging()

{

  var {:linear} l: One Loc;

  var {:linear} t: One (Tag Unit);

 

  call l, t := Tag_New();

  assert t->val->loc == l->val;

}

 

procedure ManyTags(vals: [int]bool)

{

  var {:linear} l: One Loc;

  var {:linear} ts: UnitMap (One (Tag int));

 

  call l, ts := Tags_New(vals);

  assert (forall v: int :: vals[v] ==> Map_Contains(ts, One(Tag(l->val, v))));

}

boogie /lib:base lin-loc.bpl

lin-loc.bpl(8,3): Error: this assertion could not be proved

Execution trace:

    lin-loc.bpl(6,3): anon0

    base.bpl(292,3): inline$Loc_New$0$anon0

    base.bpl(292,3): inline$Loc_New$1$anon0

    lin-loc.bpl(6,3): anon0$2

 

Boogie program verifier finished with 2 verified, 1 error

Freshness in real code comes from somewhere else: the linear type system guarantees that permissions of simultaneously-available linear variables are disjoint, and Civl injects the corresponding assume at procedure entry, at loop headers and after parallel calls (not after ordinary calls). More practically, the idiom used throughout Test/civl/ is to allocate and immediately insert:

call one_loc := Loc_New();

call Map_Put(list->nodes, one_loc, node);

at which point the Map_Put rewriting supplies assume !Map_Contains(list->nodes, one_loc) — freshness relative to the structure you care about, which is what the proof actually needs.

11.9.5 Move, Copy, Assume, Assert🔗

/// Helpers

pure procedure Copy<T>(v: T) returns (v': T);

ensures v' == v;

 

pure procedure Assume(b: bool);

ensures b;

 

pure action Assert(b: bool)

{

  assert b;

}

procedure Copying(x: Vec int) returns (y: Vec int)

{

  call y := Copy(x);

  assert y == x;

}

 

// Assume has no body and an unconditional postcondition, so it assumes anything.

procedure Assuming()

{

  call Assume(false);

  assert 1 == 2;

}

 

// Without the call to Assume the same assertion fails.

procedure NotAssuming()

{

  assert 1 == 2;

}

boogie /lib:base helpers.bpl

helpers.bpl(17,3): Error: this assertion could not be proved

Execution trace:

    helpers.bpl(17,3): anon0

 

Boogie program verifier finished with 2 verified, 1 error

The Move idiom, and the restriction on its arguments:

type Res;

 

// The Move idiom: hand a freshly split sub-map to a {:linear_out} parameter.

pure action Extract({:linear_in} pool: UnitMap (One Res), {:linear_out} l: UnitMap (One Res))

  returns ({:linear} pool': UnitMap (One Res))

{

  var _l: UnitMap (One Res);

  assert Set_IsSubset(l->dom, pool->dom);

  pool' := pool;

  call _l := Map_Split(pool', l->dom);

  call Move(_l, l);

}

 

// Move requires both arguments to be plain variables.

pure action BadMove({:linear_in} pool: UnitMap (One Res), {:linear_out} l: UnitMap (One Res))

{

  call Move(pool, Map_Empty());

}

boogie /lib:base move.bpl

move.bpl(17,2): Error: argument at position 1 must be a variable

move.bpl(17,2): Error: only variable can be passed to linear parameter: Map_Empty_3201_2239()

2 type checking errors detected in move.bpl

11.9.6 Map well-formedness is free in Civl🔗

One more thing the Civl pipeline does for you: for every available linear variable of type Map K V, it assumes Map_WellFormed at procedure entry, at loop headers and after parallel calls. Outside Civl you get nothing:

procedure Plain({:linear} a: Map int int)

{

  assert Map_WellFormed(a);

}

 

yield procedure {:layer 1} Yielding({:layer 1} {:linear} a: Map int int)

{

  assert {:layer 1} Map_WellFormed(a);

}

boogie /lib:base fmap-civl-wf.bpl

fmap-civl-wf.bpl(3,3): Error: this assertion could not be proved

Execution trace:

    fmap-civl-wf.bpl(3,3): anon0

 

Boogie program verifier finished with 2 verified, 1 error

11.10 The node library🔗

/lib:node adds a singly-linked-list node type, a reachability axiomatisation in the style of Nelson’s Between predicate, and three abstraction functions with framing lemmas. It requires /lib:base.

11.10.1 Node, Between and Avoiding🔗

datatype Node<T> { Node(next: Option Loc, val: T) }

 

function Between<T>(f: [One Loc]Node T, x: Option Loc, y: Option Loc, z: Option Loc): bool;

function Avoiding<T>(f: [One Loc]Node T, x: Option Loc, y: Option Loc, z: Option Loc): bool;

function {:inline} BetweenSet<T>(f:[One Loc]Node T, x: Option Loc, z: Option Loc): [Loc]bool

{

  (lambda y: Loc :: Between(f, x, Some(y), z))

}

A node has a next: Option Loc (with None() as null) and a payload val. The heap is modelled as a map f: [One Loc]Node T — indexed by One Loc rather than Loc, so that the same map can serve as the val component of a linear Map (One Loc) (Node T).

Both predicates are uninterpreted and are characterised by fourteen axioms. In source order they are: reflexive (Between(f, x, x, x)), step (one next hop is reachable), reach (reachability decomposes through one hop), cycle (a self-loop reaches only itself), sandwich (Between(f, x, y, x) implies x == y), order1 and order2 (the reachable set from a point is totally ordered, and a three-point Between splits into two two-point ones), transitive1, transitive2 and transitive3, one extra axiom that the source itself annotates —

// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.

// It cannot be proved using the rest of the axioms.

axiom {:ctor "Node"} (forall<T> f: [One Loc]Node T, u: Option Loc, x: Option Loc ::

  {Between(f, u, x, x)}

  Between(f, u, x, x) ==> Between(f, u, u, x));

— two axioms relating Avoiding to Between in both directions, and finally the update axiom, which is the load-bearing one: it says how Avoiding behaves in a heap f[One(p) := q] with one node replaced.

// update

axiom {:ctor "Node"} (forall<T> f: [One Loc]Node T, u: Option Loc, v: Option Loc, x: Option Loc, p: Loc, q: Node T ::

  {Avoiding(f[One(p) := q], u, v, x)}

  Avoiding(f[One(p) := q], u, v, x) <==>

    (Avoiding(f, u, v, Some(p)) && Avoiding(f, u, v, x)) ||

    (Avoiding(f, u, Some(p), x) && Some(p) != x && Avoiding(f, q->next, v, Some(p)) && Avoiding(f, q->next, v, x))

);

Every one of these axioms carries the vestigial {:ctor "Node"} attribute, which as noted above nothing reads.

type X;

 

procedure Reflexive(f: [One Loc]Node X, x: Option Loc)

{

  assert Between(f, x, x, x);

}

 

procedure Step(f: [One Loc]Node X, x: Loc)

{

  assert Between(f, Some(x), f[One(x)]->next, f[One(x)]->next);

}

 

procedure Sandwich(f: [One Loc]Node X, x: Option Loc, y: Option Loc)

requires Between(f, x, y, x);

{

  assert x == y;

}

 

procedure Transitive(f: [One Loc]Node X, x: Option Loc, y: Option Loc, z: Option Loc)

requires Between(f, x, y, y);

requires Between(f, y, z, z);

{

  assert Between(f, x, z, z);

}

 

procedure AvoidingLink(f: [One Loc]Node X, x: Option Loc, y: Option Loc, z: Option Loc)

{

  assert Between(f, x, y, z) <==> Avoiding(f, x, y, z) && Avoiding(f, x, z, z);

}

 

procedure Reachable(f: [One Loc]Node X, x: Option Loc, y: Loc)

requires Between(f, x, Some(y), None());

{

  assert BetweenSet(f, x, None())[y];

}

 

// Both ends of the range are in BetweenSet.

procedure EndpointIncluded(f: [One Loc]Node X, x: Option Loc, w: Loc)

requires Between(f, x, Some(w), Some(w));

{

  assert BetweenSet(f, x, Some(w))[w];

}

 

procedure StartIncluded(f: [One Loc]Node X, u: Loc, z: Option Loc)

requires Between(f, Some(u), z, z);

{

  assert BetweenSet(f, Some(u), z)[u];

}

boogie /lib:base /lib:node node-between.bpl

 

Boogie program verifier finished with 8 verified, 0 errors

11.10.2 InDomain🔗

function {:inline} InDomain<V>(nodes: Map (One Loc) (Node V), start: Option Loc): bool {

  Between(nodes->val, start, start, None()) &&

  (forall x: Loc:: Between(nodes->val, start, Some(x), None()) ==> Set_Contains(nodes->dom, One(x)))

}

"The list starting at start is null-terminated and every node on it is in the finite map’s domain." This is the standard well-formedness precondition for the abstraction lemmas below.

11.10.3 Stack, set and queue abstractions🔗

The library provides three abstraction functions with the same shape. Each comes as an uninterpreted function XAbs, an inlined one-step unfolding XAbsDef, and two lemmas.

/// Stack abstraction

function StackAbs<V>(start: Option Loc, nodes: Map (One Loc) (Node V)): Vec V;

function {:inline} StackAbsDef<V>(start: Option Loc, nodes: Map (One Loc) (Node V)): Vec V {

if start == None() then

  Vec_Empty() else

  (var n := Map_At(nodes, One(start->t)); Vec_Append(StackAbs(n->next, nodes), n->val))

}

 

pure procedure StackAbsLemma<V>(start: Option Loc, nodes: Map (One Loc) (Node V));

requires Between(nodes->val, start, start, None());

requires InDomain(nodes, start);

ensures StackAbs(start, nodes) == StackAbsDef(start, nodes);

 

pure procedure StackFrameLemma<V>(start: Option Loc, nodes: Map (One Loc) (Node V), nodes': Map (One Loc) (Node V));

requires Set_IsSubset(nodes->dom, nodes'->dom);

requires MapIte(nodes->dom, nodes->val, MapConst(Default())) ==

         MapIte(nodes->dom, nodes'->val, MapConst(Default()));

requires Between(nodes->val, start, start, None());

requires InDomain(nodes, start);

ensures StackAbs(start, nodes) == StackAbs(start, nodes');

The key design point: StackAbs is an uninterpreted function, and StackAbsDef is its intended defining equation, but nothing connects them until you call StackAbsLemma. This avoids putting a recursive definition directly into the background theory. The frame lemma says the abstraction is unchanged when the map grows, provided the values on the old domain are unchanged.

type X;

 

procedure Abs(nodes: Map (One Loc) (Node X), l: Loc, x: X)

requires Map_Contains(nodes, One(l));

requires Map_At(nodes, One(l)) == Node(None(), x);

requires InDomain(nodes, Some(l));

{

  call StackAbsLemma(Some(l), nodes);

  call StackAbsLemma(None(), nodes);

  assert StackAbs(Some(l), nodes) == Vec_Append(Vec_Empty(), x);

  call SetAbsLemma(Some(l), nodes);

  call SetAbsLemma(None(), nodes);

  assert SetAbs(Some(l), nodes) == Set_Singleton(x);

}

 

procedure WithoutLemma(nodes: Map (One Loc) (Node X), l: Loc, x: X)

requires Map_Contains(nodes, One(l));

requires Map_At(nodes, One(l)) == Node(None(), x);

requires InDomain(nodes, Some(l));

{

  assert StackAbs(Some(l), nodes) == Vec_Append(Vec_Empty(), x);

}

boogie /lib:base /lib:node node-abs.bpl

node-abs.bpl(21,3): Error: this assertion could not be proved

Execution trace:

    node-abs.bpl(21,3): anon0

 

Boogie program verifier finished with 1 verified, 1 error

Note that you need one lemma call per list node visited, including the terminating None() step — the lemma unfolds StackAbs exactly one level.

11.10.4 The lemmas are trusted unless you discharge them🔗

All six *AbsLemma and *FrameLemma declarations in node.bpl are body-less pure procedures, so by default their postconditions are assumed. They can be proved. Test/civl/large-samples/node-lemmas.bpl supplies implementations for all six by writing a recursive pure procedure that walks the list, using the Between axioms to argue that the recursion terminates:

implementation StackAbsLemma<V>(start: Option Loc, nodes: Map (One Loc) (Node V))

{

  var absStack: Vec V;

  call absStack := StackAbsCompute(start, nodes, nodes);

}

boogie /lib:base /lib:node node-lemmas.bpl

 

Boogie program verifier finished with 9 verified, 0 errors

If you use /lib:node in a program where soundness matters, copying that file in is the way to turn the assumptions into proofs.

11.11 Divergences from This is Boogie 2🔗

The standard library postdates This is Boogie 2 entirely, so there is nothing in the paper to contradict. One paper claim is nonetheless relevant to using the library:

11.12 Where to find real usage🔗

    contents    up