BSeq
Reference for mo:core/pure/BSeq in the core library.
BSeq.XSeq<T> is the immutable persistent-data-structure sequence used by several core proof patterns.
Spec.model maps it to the verifier's ghost Seq<T>, and the exported lemmas
bridge runtime operations such as append, update, and slice to sequence
facts. Array and list conversions are snapshot surfaces: toArray exposes
Spec.arrayToSeq(result) == Spec.model(seq), and model_from_toList bridges
fromList(toList(seq)) back to the same sequence model.
When T is an opaque/token handle, BSeq stores handle identities. The model
can prove sequence position and membership facts for those handles, but it does
not expose or freeze the owner's sealed payload behind each handle.
Import
mo:core/pure/BSeq
Status
- Pure immutable collection module
Public API
Types
Node,LeafNode,RegularNode,RelaxedNode,XSeq,Frozen,IterDirection,NodeCursor,IterState
Modules
Spec
Functions
empty<T>() : XSeq<T>
Constructs the empty value for this module's data structure.
Contract
ensures Spec.model<T>(result) == Seq.empty<T>();
ensures len<T>(result) == 0;
Use when: code or specifications need this operation with the documented contract.
singleton<T>(value : T) : XSeq<T>
Constructs a value containing exactly the supplied element or entry.
Contract
ensures Spec.model<T>(result) == Seq.singleton<T>(value);
ensures len<T>(result) == 1;
ensures get<T>(result, 0) == value;
Use when: code or specifications need this operation with the documented contract.
len<T>(seq : XSeq<T>) : Int
Returns the length or cardinality represented by the value.
Contract
ensures result == Seq.len<T>(Spec.model<T>(seq));
ensures result == (seq.len : Int);
ensures result >= 0;
Use when: code or specifications need this operation with the documented contract.
size<T>(seq : XSeq<T>) : Nat
Returns the length or cardinality represented by the value.
Contract
ensures result == seq.len;
ensures len<T>(seq) == (result : Int);
Use when: code or specifications need this operation with the documented contract.
foldLeft<T, A>(seq : XSeq<T>, base : A, combine : (A, T) -> A) : A
Folds the structure by applying the supplied accumulator function.
Contract
ensures len<T>(seq) == 0 ==> result == base;
Use when: code or specifications need this operation with the documented contract.
get<T>(seq : XSeq<T>, index : Int) : T
Reads the requested value from the structure.
Contract
requires index >= 0;
requires index < len<T>(seq);
ensures result == Seq.get<T>(Spec.model<T>(seq), index);
Use when: reading this value is part of an implementation or postcondition.
getNat<T>(seq : XSeq<T>, index : Nat) : T
Reads the requested value from the structure.
Contract
requires (index : Int) >= 0;
requires index < size<T>(seq);
ensures result == get<T>(seq, index : Int);
Use when: reading this value is part of an implementation or postcondition.
freeze<T>(seq : XSeq<T>) : Frozen<T>
Converts or copies the persistent builder/tree representation.
Contract
ensures Spec.arrayToSeq<T>(result.items) == Spec.model<T>(seq);
ensures result.count == size<T>(seq);
ensures result.count == result.items.size();
Use when: code or specifications need this operation with the documented contract.
update<T>(seq : XSeq<T>, index : Int, value : T) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
requires index >= 0;
requires index < len<T>(seq);
ensures Spec.model<T>(result) == Seq.update<T>(Spec.model<T>(seq), index, value);
ensures len<T>(result) == len<T>(seq);
ensures get<T>(result, index) == value;
Use when: the postcondition must relate the updated value to the previous one.
set<T>(seq : XSeq<T>, index : Int, value : T) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
requires index >= 0;
requires index < len<T>(seq);
ensures Spec.model<T>(result) == Seq.update<T>(Spec.model<T>(seq), index, value);
ensures len<T>(result) == len<T>(seq);
ensures get<T>(result, index) == value;
Use when: the postcondition must relate the updated value to the previous one.
append<T>(seq : XSeq<T>, value : T) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
ensures Spec.model<T>(result) == Seq.concat<T>(Spec.model<T>(seq), Seq.singleton<T>(value));
ensures len<T>(result) == len<T>(seq) + 1;
ensures get<T>(result, len<T>(seq)) == value;
Use when: the postcondition must relate the updated value to the previous one.
take<T>(seq : XSeq<T>, n : Int) : XSeq<T>
Returns the updated collection or value described by the contract.
Contract
requires n >= 0;
ensures Spec.model<T>(result) == Seq.take<T>(Spec.model<T>(seq), n);
Use when: the postcondition must relate the updated value to the previous one.
drop<T>(seq : XSeq<T>, n : Int) : XSeq<T>
Returns the updated collection or value described by the contract.
Contract
requires n >= 0;
ensures Spec.model<T>(result) == Seq.drop<T>(Spec.model<T>(seq), n);
Use when: the postcondition must relate the updated value to the previous one.
slice<T>(seq : XSeq<T>, i : Int, j : Int) : XSeq<T>
Implements the slice helper described by its signature and contract.
Contract
requires i >= 0;
requires j >= i;
ensures Spec.model<T>(result) == Seq.take<T>(Seq.drop<T>(Spec.model<T>(seq), i), j - i);
Use when: code or specifications need this operation with the documented contract.
concat<T>(left : XSeq<T>, right : XSeq<T>) : XSeq<T>
Implements the concat helper described by its signature and contract.
Contract
ensures Spec.model<T>(result) == Seq.concat<T>(Spec.model<T>(left), Spec.model<T>(right));
ensures len<T>(result) == len<T>(left) + len<T>(right);
Use when: code or specifications need this operation with the documented contract.
appendAll<T>(seq : XSeq<T>, arr : [T]) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
ensures Spec.model<T>(result) == Seq.concat<T>(Spec.model<T>(seq), Spec.arrayToSeq<T>(arr));
Use when: the postcondition must relate the updated value to the previous one.
prepend<T>(seq : XSeq<T>, value : T) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
ensures Spec.model<T>(result) == Seq.concat<T>(Seq.singleton<T>(value), Spec.model<T>(seq));
ensures len<T>(result) == len<T>(seq) + 1;
ensures get<T>(result, 0) == value;
Use when: the postcondition must relate the updated value to the previous one.
prependAll<T>(seq : XSeq<T>, arr : [T]) : XSeq<T>
Returns or applies the corresponding update to the structure.
Contract
ensures Spec.model<T>(result) == Seq.concat<T>(Spec.arrayToSeq<T>(arr), Spec.model<T>(seq));
Use when: the postcondition must relate the updated value to the previous one.
first<T>(seq : XSeq<T>) : ?T
Reads the requested value from the structure.
Contract
ensures len<T>(seq) == 0 ==> result == null;
ensures len<T>(seq) > 0 ==> result == ?get<T>(seq, 0);
Use when: reading this value is part of an implementation or postcondition.
last<T>(seq : XSeq<T>) : ?T
Reads the requested value from the structure.
Contract
ensures len<T>(seq) == 0 ==> result == null;
ensures len<T>(seq) > 0 ==> result == ?get<T>(seq, (len<T>(seq) - 1) : Int);
Use when: reading this value is part of an implementation or postcondition.
popFirst<T>(seq : XSeq<T>) : (?T, XSeq<T>)
Returns the updated collection or value described by the contract.
Contract
ensures len<T>(seq) == 0 ==> (result.0 == null and result.1 == seq);
ensures len<T>(seq) > 0 ==>
(result.0 == ?Seq.get<T>(Spec.model<T>(seq), 0)
and Spec.model<T>(result.1) == Seq.drop<T>(Spec.model<T>(seq), 1));
Use when: the postcondition must relate the updated value to the previous one.
popLast<T>(seq : XSeq<T>) : (?T, XSeq<T>)
Returns the updated collection or value described by the contract.
Contract
ensures len<T>(seq) == 0 ==> (result.0 == null and result.1 == seq);
ensures len<T>(seq) == 0 ==> len<T>(result.1) == 0;
ensures len<T>(seq) > 0 ==>
(result.0 == ?Seq.get<T>(Spec.model<T>(seq), len<T>(seq) - 1)
and Spec.model<T>(result.1) == Seq.take<T>(Spec.model<T>(seq), len<T>(seq) - 1));
ensures len<T>(seq) > 0 ==> len<T>(result.1) == len<T>(seq) - 1;
ensures len<T>(result.1) <= len<T>(seq);
ensures size<T>(result.1) <= size<T>(seq);
Use when: the postcondition must relate the updated value to the previous one.
contains<T>(value : T, seq : XSeq<T>, equal : (T, T) -> Bool) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == Spec.seqContains<T>(value, Spec.model<T>(seq));
Use when: a branch condition or contract needs this predicate as a named fact.
sorted(seq : XSeq<Nat>) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == Spec.seqSorted(Spec.model<Nat>(seq));
Use when: code or specifications need this operation with the documented contract.
sortedBy<T>(seq : XSeq<T>, compare : (T, T) -> Types.Order) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == Spec.seqSortedBy<T>(Spec.model<T>(seq), compare);
Use when: code or specifications need this operation with the documented contract.
sortedByDesc<T>(seq : XSeq<T>, compare : (T, T) -> Types.Order) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == Spec.seqSortedByDesc<T>(Spec.model<T>(seq), compare);
Use when: code or specifications need this operation with the documented contract.
permutes<T>(a : XSeq<T>, b : XSeq<T>, equal : (T, T) -> Bool) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == Spec.seqPermutes<T>(Spec.model<T>(a), Spec.model<T>(b));
Use when: code or specifications need this operation with the documented contract.
iter<T>(seq : XSeq<T>) : Types.Iter<T>
Implements the iter helper described by its signature and contract.
Use when: code or specifications need this operation with the documented contract.
fromList<T>(list : Types.Pure.List<T>) : XSeq<T>
Converts between the module type and the target representation.
Contract
ensures Spec.model<T>(result) == Spec.listToSeq<T>(list);
Use when: crossing between this module's value and another representation.
toList<T>(seq : XSeq<T>) : Types.Pure.List<T>
Converts between the module type and the target representation.
Contract
ensures result == Spec.seqToList<T>(Spec.model<T>(seq));
Use when: crossing between this module's value and another representation.
toArray<T>(seq : XSeq<T>) : [T]
Converts between the module type and the target representation.
Contract
ensures Spec.arrayToSeq<T>(result) == Spec.model<T>(seq);
ensures result.size() == seq.len;
Use when: crossing between this module's value and another representation.
fromArray<T>(arr : [T]) : XSeq<T>
Converts between the module type and the target representation.
Contract
ensures Spec.model<T>(result) == Spec.arrayToSeq<T>(arr);
Use when: crossing between this module's value and another representation.
Lemmas
model_empty<T>() : ()
Establishes Spec.model<T>(empty<T>()) == Seq.empty<T>() in the current proof context.
Contract
ensures Spec.model<T>(empty<T>()) == Seq.empty<T>();
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_singleton<T>(value : T) : ()
Establishes Spec.model<T>(singleton<T>(value)) == Seq.singleton<T>(value) in the current proof context.
Contract
ensures Spec.model<T>(singleton<T>(value)) == Seq.singleton<T>(value);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_len<T>(seq : XSeq<T>) : ()
Establishes Seq.len<T>(Spec.model<T>(seq)) == len<T>(seq) in the current proof context.
Contract
ensures Seq.len<T>(Spec.model<T>(seq)) == len<T>(seq);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_get<T>(seq : XSeq<T>, i : Int) : ()
Establishes Seq.get<T>(Spec.model<T>(seq), i) == get<T>(seq, i) in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
requires i < Seq.len<T>(Spec.model<T>(seq));
ensures Seq.get<T>(Spec.model<T>(seq), i) == get<T>(seq, i);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_update<T>(seq : XSeq<T>, i : Int, v : T) : ()
Establishes Spec.model<T>(update<T>(seq, i, v)) == Seq.update<T>(Spec.model<T>(seq), i, v) in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
ensures Spec.model<T>(update<T>(seq, i, v)) == Seq.update<T>(Spec.model<T>(seq), i, v);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_append<T>(seq : XSeq<T>, value : T) : ()
Establishes Spec.model<T>(append<T>(seq, value)) == Seq.concat<T>(Spec.model<T>(seq), Seq.singleton<T>(value)) in the current proof context.
Contract
ensures Spec.model<T>(append<T>(seq, value)) == Seq.concat<T>(Spec.model<T>(seq), Seq.singleton<T>(value));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_prepend<T>(seq : XSeq<T>, value : T) : ()
Establishes Spec.model<T>(prepend<T>(seq, value)) == Seq.concat<T>(Seq.singleton<T>(value), Spec.model<T>(seq)) in the current proof context.
Contract
ensures Spec.model<T>(prepend<T>(seq, value)) == Seq.concat<T>(Seq.singleton<T>(value), Spec.model<T>(seq));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_concat<T>(left : XSeq<T>, right : XSeq<T>) : ()
Establishes Spec.model<T>(concat<T>(left, right)) == Seq.concat<T>(Spec.model<T>(left), Spec.model<T>(right)) in the current proof context.
Contract
ensures Spec.model<T>(concat<T>(left, right)) == Seq.concat<T>(Spec.model<T>(left), Spec.model<T>(right));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_take<T>(seq : XSeq<T>, n : Int) : ()
Establishes Spec.model<T>(take<T>(seq, n)) == Seq.take<T>(Spec.model<T>(seq), n) in the current proof context.
Contract
requires n >= 0;
ensures Spec.model<T>(take<T>(seq, n)) == Seq.take<T>(Spec.model<T>(seq), n);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_drop<T>(seq : XSeq<T>, n : Int) : ()
Establishes Spec.model<T>(drop<T>(seq, n)) == Seq.drop<T>(Spec.model<T>(seq), n) in the current proof context.
Contract
requires n >= 0;
ensures Spec.model<T>(drop<T>(seq, n)) == Seq.drop<T>(Spec.model<T>(seq), n);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_slice<T>(seq : XSeq<T>, i : Int, j : Int) : ()
Establishes Spec.model<T>(slice<T>(seq, i, j)) == Seq.take<T>(Seq.drop<T>(Spec.model<T>(seq), i), j - i) in the current proof context.
Contract
requires i >= 0;
requires j >= i;
ensures Spec.model<T>(slice<T>(seq, i, j)) == Seq.take<T>(Seq.drop<T>(Spec.model<T>(seq), i), j - i);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_fromArray<T>(arr : [T]) : ()
Establishes Spec.model<T>(fromArray<T>(arr)) == Spec.arrayToSeq<T>(arr) in the current proof context.
Contract
ensures Spec.model<T>(fromArray<T>(arr)) == Spec.arrayToSeq<T>(arr);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
arrayToSeq_len<T>(arr : [T]) : ()
Establishes Seq.len<T>(Spec.arrayToSeq<T>(arr)) == (arr.size() : Int) in the current proof context.
Contract
ensures Seq.len<T>(Spec.arrayToSeq<T>(arr)) == (arr.size() : Int);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
arrayToSeq_get<T>(arr : [T], i : Nat) : ()
Establishes Seq.get<T>(Spec.arrayToSeq<T>(arr), (i : Int)) == arr[i] in the current proof context.
Contract
requires i < arr.size();
requires (i : Int) < Seq.len<T>(Spec.arrayToSeq<T>(arr));
ensures Seq.get<T>(Spec.arrayToSeq<T>(arr), (i : Int)) == arr[i];
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_fromArray_len<T>(arr : [T]) : ()
Establishes Seq.len<T>(Spec.model<T>(fromArray<T>(arr))) == (arr.size() : Int) in the current proof context.
Contract
ensures Seq.len<T>(Spec.model<T>(fromArray<T>(arr))) == (arr.size() : Int);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_fromArray_get<T>(arr : [T], i : Nat) : ()
Establishes Seq.get<T>(Spec.model<T>(fromArray<T>(arr)), (i : Int)) == arr[i] in the current proof context.
Contract
requires i < arr.size();
requires (i : Int) < Seq.len<T>(Spec.model<T>(fromArray<T>(arr)));
ensures Seq.get<T>(Spec.model<T>(fromArray<T>(arr)), (i : Int)) == arr[i];
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
arrayToSeq_toArray_len<T>(seq : XSeq<T>) : ()
Establishes Seq.len<T>(Spec.arrayToSeq<T>(toArray<T>(seq))) == len<T>(seq) in the current proof context.
Contract
ensures Seq.len<T>(Spec.arrayToSeq<T>(toArray<T>(seq))) == len<T>(seq);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
arrayToSeq_toArray_get<T>(seq : XSeq<T>, i : Int) : ()
Establishes Seq.get<T>(Spec.arrayToSeq<T>(toArray<T>(seq)), i) == get<T>(seq, i) in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
requires i < Seq.len<T>(Spec.arrayToSeq<T>(toArray<T>(seq)));
ensures Seq.get<T>(Spec.arrayToSeq<T>(toArray<T>(seq)), i) == get<T>(seq, i);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_fromList<T>(list : Types.Pure.List<T>) : ()
Establishes Spec.model<T>(fromList<T>(list)) == Spec.listToSeq<T>(list) in the current proof context.
Contract
ensures Spec.model<T>(fromList<T>(list)) == Spec.listToSeq<T>(list);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_from_toList<T>(seq : XSeq<T>) : ()
Establishes Spec.model<T>(fromList<T>(toList<T>(seq))) == Spec.model<T>(seq) in the current proof context.
Contract
ensures Spec.model<T>(fromList<T>(toList<T>(seq))) == Spec.model<T>(seq);
Use when: a proof converts an XSeq to a pure list and then back to an XSeq, and needs the list-shaped snapshot tied to the original ordered model.
model_appendAll<T>(seq : XSeq<T>, arr : [T]) : ()
Establishes Spec.model<T>(appendAll<T>(seq, arr)) == Seq.concat<T>(Spec.model<T>(seq), Spec.arrayToSeq<T>(arr)) in the current proof context.
Contract
ensures Spec.model<T>(appendAll<T>(seq, arr)) == Seq.concat<T>(Spec.model<T>(seq), Spec.arrayToSeq<T>(arr));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_prependAll<T>(seq : XSeq<T>, arr : [T]) : ()
Establishes Spec.model<T>(prependAll<T>(seq, arr)) == Seq.concat<T>(Spec.arrayToSeq<T>(arr), Spec.model<T>(seq)) in the current proof context.
Contract
ensures Spec.model<T>(prependAll<T>(seq, arr)) == Seq.concat<T>(Spec.arrayToSeq<T>(arr), Spec.model<T>(seq));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_popFirst<T>(seq : XSeq<T>) : ()
Establishes the listed proof facts in the current verification context.
Contract
requires len<T>(seq) > 0;
ensures Spec.model<T>(popFirst<T>(seq).1) == Seq.drop<T>(Spec.model<T>(seq), 1);
ensures popFirst<T>(seq).0 == ?Seq.get<T>(Spec.model<T>(seq), 0);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
model_popLast<T>(seq : XSeq<T>) : ()
Establishes the listed proof facts in the current verification context.
Contract
requires len<T>(seq) > 0;
ensures Spec.model<T>(popLast<T>(seq).1) == Seq.take<T>(Spec.model<T>(seq), len<T>(seq) - 1);
ensures popLast<T>(seq).0 == ?Seq.get<T>(Spec.model<T>(seq), len<T>(seq) - 1);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
sorted_model(seq : XSeq<Nat>) : ()
Establishes sorted(seq) == Spec.seqSorted(Spec.model<Nat>(seq)) in the current proof context.
Contract
ensures sorted(seq) == Spec.seqSorted(Spec.model<Nat>(seq));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
permutes_model<T>(a : XSeq<T>, b : XSeq<T>, equal : (T, T) -> Bool) : ()
Establishes permutes<T>(a, b, equal) == Spec.seqPermutes<T>(Spec.model<T>(a), Spec.model<T>(b)) in the current proof context.
Contract
ensures permutes<T>(a, b, equal) == Spec.seqPermutes<T>(Spec.model<T>(a), Spec.model<T>(b));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
contains_model<T>(value : T, seq : XSeq<T>, equal : (T, T) -> Bool) : ()
Establishes contains<T>(value, seq, equal) == Spec.seqContains<T>(value, Spec.model<T>(seq)) in the current proof context.
Contract
ensures contains<T>(value, seq, equal) == Spec.seqContains<T>(value, Spec.model<T>(seq));
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_empty<T>() : ()
Establishes len<T>(empty<T>()) == 0 in the current proof context.
Contract
ensures len<T>(empty<T>()) == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_singleton<T>(value : T) : ()
Establishes len<T>(singleton<T>(value)) == 1 in the current proof context.
Contract
ensures len<T>(singleton<T>(value)) == 1;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_append<T>(seq : XSeq<T>, value : T) : ()
Establishes len<T>(append<T>(seq, value)) == len<T>(seq) + 1 in the current proof context.
Contract
ensures len<T>(append<T>(seq, value)) == len<T>(seq) + 1;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_prepend<T>(seq : XSeq<T>, value : T) : ()
Establishes len<T>(prepend<T>(seq, value)) == len<T>(seq) + 1 in the current proof context.
Contract
ensures len<T>(prepend<T>(seq, value)) == len<T>(seq) + 1;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_concat<T>(left : XSeq<T>, right : XSeq<T>) : ()
Establishes len<T>(concat<T>(left, right)) == len<T>(left) + len<T>(right) in the current proof context.
Contract
ensures len<T>(concat<T>(left, right)) == len<T>(left) + len<T>(right);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
len_update<T>(seq : XSeq<T>, i : Int, v : T) : ()
Establishes len<T>(update<T>(seq, i, v)) == len<T>(seq) in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
ensures len<T>(update<T>(seq, i, v)) == len<T>(seq);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
get_update_same<T>(seq : XSeq<T>, i : Int, v : T) : ()
Establishes get<T>(update<T>(seq, i, v), i) == v in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
ensures get<T>(update<T>(seq, i, v), i) == v;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
get_update_other<T>(seq : XSeq<T>, i : Int, j : Int, v : T) : ()
Establishes get<T>(update<T>(seq, i, v), j) == get<T>(seq, j) in the current proof context.
Contract
requires i >= 0;
requires i < len<T>(seq);
requires j >= 0;
requires j < len<T>(seq);
requires i != j;
ensures get<T>(update<T>(seq, i, v), j) == get<T>(seq, j);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
get_append_last<T>(seq : XSeq<T>, value : T) : ()
Establishes get<T>(append<T>(seq, value), len<T>(seq)) == value in the current proof context.
Contract
requires len<T>(seq) < len<T>(append<T>(seq, value));
ensures get<T>(append<T>(seq, value), len<T>(seq)) == value;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
get_prepend_first<T>(seq : XSeq<T>, value : T) : ()
Establishes get<T>(prepend<T>(seq, value), 0) == value in the current proof context.
Contract
requires 0 < len<T>(prepend<T>(seq, value));
ensures get<T>(prepend<T>(seq, value), 0) == value;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
foldLeft_empty<T, A>(base : A, combine : (A, T) -> A) : ()
Establishes foldLeft<T, A>(empty<T>(), base, combine) == base in the current proof context.
Contract
ensures foldLeft<T, A>(empty<T>(), base, combine) == base;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
foldLeft_singleton<T, A>(value : T, base : A, combine : (A, T) -> A) : ()
Establishes foldLeft<T, A>(singleton<T>(value), base, combine) == combine(base, value) in the current proof context.
Contract
ensures foldLeft<T, A>(singleton<T>(value), base, combine) == combine(base, value);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
foldLeft_append<T, A>(seq : XSeq<T>, value : T, base : A, combine : (A, T) -> A) : ()
Establishes foldLeft<T, A>(append<T>(seq, value), base, combine) == combine(foldLeft<T, A>(seq, base, combine), value) in the current proof context.
Contract
ensures foldLeft<T, A>(append<T>(seq, value), base, combine) ==
combine(foldLeft<T, A>(seq, base, combine), value);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
Spec Module
Spec Functions
model<T>(seq : XSeq<T>) : Seq<T>
Returns the abstract ghost model used by contracts and lemmas.
For handle elements, this is an identity model: it records the sequence of handles, not snapshots of owner payload models.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
arrayToSeq<T>(arr : [T]) : Seq<T>
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
listToSeq<T>(list : Types.Pure.List<T>) : Seq<T>
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqToList<T>(seq : Seq<T>) : Types.Pure.List<T>
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqSorted(seq : Seq<Nat>) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqSortedBy<T>(seq : Seq<T>, compare : (T, T) -> Types.Order) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqSortedByDesc<T>(seq : Seq<T>, compare : (T, T) -> Types.Order) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqSortedByTake<T>(seq : Seq<T>, compare : (T, T) -> Types.Order, n : Int) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Contract
requires n >= 0;
ensures result;
ensures seqSortedBy<T>(seq, compare) ==> seqSortedBy<T>(Seq.take<T>(seq, n), compare);
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqSortedByDescTake<T>(seq : Seq<T>, compare : (T, T) -> Types.Order, n : Int) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Contract
requires n >= 0;
ensures result;
ensures seqSortedByDesc<T>(seq, compare) ==> seqSortedByDesc<T>(Seq.take<T>(seq, n), compare);
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqPermutes<T>(a : Seq<T>, b : Seq<T>) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
seqContains<T>(value : T, seq : Seq<T>) : Bool
Provides a ghost/spec-only abstraction for contracts and proofs.
Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.
Summary
- Pure immutable collection module under
mo:core/pure/BSeq. - Exposes 32 public functions.
- Exposes 39 trusted lemmas.
- Includes 11 spec helpers in
Spec.