Potential unsoundness
Closed this issue · 0 comments
marcoeilers commented
The following program verifies in Silicon but not in Carbon (and I think Carbon is right):
domain PyType {
function extends_(sub: PyType, super: PyType): Bool
function issubtype(sub: PyType, super: PyType): Bool
function isnotsubtype(sub: PyType, super: PyType): Bool
function typeof(obj: Ref): PyType
function get_basic(t: PyType): PyType
function union_type_1(arg_1: PyType): PyType
function union_type_2(arg_1: PyType, arg_2: PyType): PyType
function union_type_3(arg_1: PyType, arg_2: PyType, arg_3: PyType): PyType
function union_type_4(arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType): PyType
unique function object(): PyType
unique function list_basic(): PyType
function list(arg0: PyType): PyType
function list_arg(typ: PyType, index: Int): PyType
unique function set_basic(): PyType
function set(arg0: PyType): PyType
function set_arg(typ: PyType, index: Int): PyType
unique function dict_basic(): PyType
function dict(arg0: PyType, arg1: PyType): PyType
function dict_arg(typ: PyType, index: Int): PyType
unique function int(): PyType
unique function float(): PyType
unique function bool(): PyType
unique function NoneType(): PyType
unique function Exception(): PyType
unique function ConnectionRefusedError(): PyType
unique function traceback(): PyType
unique function str(): PyType
unique function bytes(): PyType
unique function __prim__perm(): PyType
unique function PSeq_basic(): PyType
function PSeq(arg0: PyType): PyType
function PSeq_arg(typ: PyType, index: Int): PyType
unique function PSet_basic(): PyType
function PSet(arg0: PyType): PyType
function PSet_arg(typ: PyType, index: Int): PyType
unique function PMultiset_basic(): PyType
function PMultiset(arg0: PyType): PyType
function PMultiset_arg(typ: PyType, index: Int): PyType
unique function slice(): PyType
unique function range_0(): PyType
unique function Iterator_basic(): PyType
function Iterator(arg0: PyType): PyType
function Iterator_arg(typ: PyType, index: Int): PyType
unique function Thread_0(): PyType
unique function LevelType(): PyType
unique function type(): PyType
unique function Place(): PyType
unique function __prim__Seq_type(): PyType
unique function Node(): PyType
axiom issubtype_transitivity {
(forall sub: PyType, middle: PyType, super: PyType ::
{ issubtype(sub, middle), issubtype(middle, super) }
{ issubtype(sub, super), issubtype(middle, super) }
{ issubtype(sub, middle), issubtype(sub, super) }
issubtype(sub, middle) && issubtype(middle, super) ==>
issubtype(sub, super))
}
axiom issubtype_reflexivity {
(forall type_: PyType ::
{ issubtype(type_, type_) }
issubtype(type_, type_))
}
axiom extends_implies_subtype {
(forall sub: PyType, sub2: PyType ::
{ extends_(sub, sub2) }
extends_(sub, sub2) ==> issubtype(sub, sub2))
}
axiom null_nonetype {
(forall r: Ref ::
{ typeof(r) }
issubtype(typeof(r), NoneType()) == (r == null))
}
axiom issubtype_object {
(forall type_: PyType ::
{ issubtype(type_, object()) }
issubtype(type_, object()))
}
axiom issubtype_exclusion {
(forall sub: PyType, sub2: PyType, super: PyType ::
{ extends_(sub, super), extends_(sub2, super) }
extends_(sub, super) && extends_(sub2, super) && sub != sub2 ==>
isnotsubtype(sub, sub2) && isnotsubtype(sub2, sub))
}
axiom issubtype_exclusion_2 {
(forall sub: PyType, super: PyType ::
{ issubtype(sub, super) }
{ issubtype(super, sub) }
issubtype(sub, super) && sub != super ==> !issubtype(super, sub))
}
axiom issubtype_exclusion_propagation {
(forall sub: PyType, middle: PyType, super: PyType ::
{ issubtype(sub, middle), isnotsubtype(middle, super) }
issubtype(sub, middle) && isnotsubtype(middle, super) ==>
!issubtype(sub, super))
}
axiom union_subtype_1 {
(forall arg_1: PyType, X: PyType ::
{ issubtype(X, union_type_1(arg_1)) }
issubtype(X, union_type_1(arg_1)) == (false || issubtype(X, arg_1)))
}
axiom union_subtype_2 {
(forall arg_1: PyType, arg_2: PyType, X: PyType ::
{ issubtype(X, union_type_2(arg_1, arg_2)) }
issubtype(X, union_type_2(arg_1, arg_2)) ==
(false || issubtype(X, arg_1) || issubtype(X, arg_2)))
}
axiom union_subtype_3 {
(forall arg_1: PyType, arg_2: PyType, arg_3: PyType, X: PyType ::
{ issubtype(X, union_type_3(arg_1, arg_2, arg_3)) }
issubtype(X, union_type_3(arg_1, arg_2, arg_3)) ==
(false || issubtype(X, arg_1) || issubtype(X, arg_2) ||
issubtype(X, arg_3)))
}
axiom union_subtype_4 {
(forall arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType, X: PyType ::
{ issubtype(X, union_type_4(arg_1, arg_2, arg_3, arg_4)) }
issubtype(X, union_type_4(arg_1, arg_2, arg_3, arg_4)) ==
(false || issubtype(X, arg_1) || issubtype(X, arg_2) ||
issubtype(X, arg_3) ||
issubtype(X, arg_4)))
}
axiom subtype_union_1 {
(forall arg_1: PyType, X: PyType ::
{ issubtype(union_type_1(arg_1), X) }
issubtype(union_type_1(arg_1), X) == (true && issubtype(arg_1, X)))
}
axiom subtype_union_2 {
(forall arg_1: PyType, arg_2: PyType, X: PyType ::
{ issubtype(union_type_2(arg_1, arg_2), X) }
issubtype(union_type_2(arg_1, arg_2), X) ==
(true && issubtype(arg_1, X) && issubtype(arg_2, X)))
}
axiom subtype_union_3 {
(forall arg_1: PyType, arg_2: PyType, arg_3: PyType, X: PyType ::
{ issubtype(union_type_3(arg_1, arg_2, arg_3), X) }
issubtype(union_type_3(arg_1, arg_2, arg_3), X) ==
(true && issubtype(arg_1, X) && issubtype(arg_2, X) &&
issubtype(arg_3, X)))
}
axiom subtype_union_4 {
(forall arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType, X: PyType ::
{ issubtype(union_type_4(arg_1, arg_2, arg_3, arg_4), X) }
issubtype(union_type_4(arg_1, arg_2, arg_3, arg_4), X) ==
(true && issubtype(arg_1, X) && issubtype(arg_2, X) &&
issubtype(arg_3, X) &&
issubtype(arg_4, X)))
}
axiom subtype_list {
(forall var0: PyType ::
{ list(var0) }
extends_(list(var0), object()) &&
get_basic(list(var0)) == list_basic())
}
axiom list_args0 {
(forall Z: PyType, arg0: PyType ::
{ list(arg0), list_arg(Z, 0) }
issubtype(Z, list(arg0)) ==> list_arg(Z, 0) == arg0)
}
axiom subtype_set {
(forall var0: PyType ::
{ set(var0) }
extends_(set(var0), object()) && get_basic(set(var0)) == set_basic())
}
axiom set_args0 {
(forall Z: PyType, arg0: PyType ::
{ set(arg0), set_arg(Z, 0) }
issubtype(Z, set(arg0)) ==> set_arg(Z, 0) == arg0)
}
axiom subtype_dict {
(forall var0: PyType, var1: PyType ::
{ dict(var0, var1) }
extends_(dict(var0, var1), object()) &&
get_basic(dict(var0, var1)) == dict_basic())
}
axiom dict_args0 {
(forall Z: PyType, arg0: PyType, arg1: PyType ::
{ dict(arg0, arg1), dict_arg(Z, 0) }
issubtype(Z, dict(arg0, arg1)) ==> dict_arg(Z, 0) == arg0)
}
axiom dict_args1 {
(forall Z: PyType, arg0: PyType, arg1: PyType ::
{ dict(arg0, arg1), dict_arg(Z, 1) }
issubtype(Z, dict(arg0, arg1)) ==> dict_arg(Z, 1) == arg1)
}
axiom subtype_int {
extends_(int(), float()) && get_basic(int()) == int()
}
axiom subtype_float {
extends_(float(), object()) && get_basic(float()) == float()
}
axiom subtype_bool {
extends_(bool(), int()) && get_basic(bool()) == bool()
}
axiom subtype_NoneType {
extends_(NoneType(), object()) && get_basic(NoneType()) == NoneType()
}
axiom subtype_Exception {
extends_(Exception(), object()) &&
get_basic(Exception()) == Exception()
}
axiom subtype_ConnectionRefusedError {
extends_(ConnectionRefusedError(), Exception()) &&
get_basic(ConnectionRefusedError()) == ConnectionRefusedError()
}
axiom subtype_traceback {
extends_(traceback(), object()) &&
get_basic(traceback()) == traceback()
}
axiom subtype_str {
extends_(str(), object()) && get_basic(str()) == str()
}
axiom subtype_bytes {
extends_(bytes(), object()) && get_basic(bytes()) == bytes()
}
axiom subtype___prim__perm {
extends_(__prim__perm(), object()) &&
get_basic(__prim__perm()) == __prim__perm()
}
axiom subtype_PSeq {
(forall var0: PyType ::
{ PSeq(var0) }
extends_(PSeq(var0), object()) &&
get_basic(PSeq(var0)) == PSeq_basic())
}
axiom PSeq_args0 {
(forall Z: PyType, arg0: PyType ::
{ PSeq(arg0), PSeq_arg(Z, 0) }
issubtype(Z, PSeq(arg0)) ==> PSeq_arg(Z, 0) == arg0)
}
axiom subtype_PSet {
(forall var0: PyType ::
{ PSet(var0) }
extends_(PSet(var0), object()) &&
get_basic(PSet(var0)) == PSet_basic())
}
axiom PSet_args0 {
(forall Z: PyType, arg0: PyType ::
{ PSet(arg0), PSet_arg(Z, 0) }
issubtype(Z, PSet(arg0)) ==> PSet_arg(Z, 0) == arg0)
}
axiom subtype_PMultiset {
(forall var0: PyType ::
{ PMultiset(var0) }
extends_(PMultiset(var0), object()) &&
get_basic(PMultiset(var0)) == PMultiset_basic())
}
axiom PMultiset_args0 {
(forall Z: PyType, arg0: PyType ::
{ PMultiset(arg0), PMultiset_arg(Z, 0) }
issubtype(Z, PMultiset(arg0)) ==> PMultiset_arg(Z, 0) == arg0)
}
axiom subtype_slice {
extends_(slice(), object()) && get_basic(slice()) == slice()
}
axiom subtype_range_0 {
extends_(range_0(), object()) && get_basic(range_0()) == range_0()
}
axiom subtype_Iterator {
(forall var0: PyType ::
{ Iterator(var0) }
extends_(Iterator(var0), object()) &&
get_basic(Iterator(var0)) == Iterator_basic())
}
axiom Iterator_args0 {
(forall Z: PyType, arg0: PyType ::
{ Iterator(arg0), Iterator_arg(Z, 0) }
issubtype(Z, Iterator(arg0)) ==> Iterator_arg(Z, 0) == arg0)
}
axiom subtype_Thread_0 {
extends_(Thread_0(), object()) && get_basic(Thread_0()) == Thread_0()
}
axiom subtype_LevelType {
extends_(LevelType(), object()) &&
get_basic(LevelType()) == LevelType()
}
axiom subtype_type {
extends_(type(), object()) && get_basic(type()) == type()
}
axiom subtype_Place {
extends_(Place(), object()) && get_basic(Place()) == Place()
}
axiom subtype___prim__Seq_type {
extends_(__prim__Seq_type(), object()) &&
get_basic(__prim__Seq_type()) == __prim__Seq_type()
}
axiom subtype_Node {
extends_(Node(), object()) && get_basic(Node()) == Node()
}
}
domain SIFDomain[T] {
function Low(x: T): Bool
function LowEvent(): Bool
axiom low_true {
(forall x: T :: { (Low(x): Bool) } (Low(x): Bool))
}
axiom lowevent_true {
(LowEvent(): Bool)
}
}
domain __ObjectEquality {
function object___eq__(Ref, Ref): Bool
axiom {
(forall o1: Ref, o2: Ref, o3: Ref ::
{ object___eq__(o1, o2), object___eq__(o2, o3) }
{ object___eq__(o1, o2), object___eq__(o1, o3) }
{ object___eq__(o2, o3), object___eq__(o1, o3) }
object___eq__(o1, o2) && object___eq__(o2, o3) ==>
object___eq__(o1, o3))
}
axiom {
(forall o1: Ref, o2: Ref ::
{ object___eq__(o1, o2) }
object___eq__(o1, o2) == object___eq__(o2, o1) &&
((o1 == o2 ==> object___eq__(o1, o2)) &&
((o1 == null) != (o2 == null) ==> !object___eq__(o1, o2))))
}
}
domain __SumHelper[T$] {
function __sum(s: Seq[Int]): Int
axiom __sum_def_1 {
(__sum(Seq[Int]()): Int) == 0
}
axiom __sum_def_2 {
(forall __t: Int ::
{ (__sum(Seq(__t)): Int) }
(__sum(Seq(__t)): Int) == __t)
}
axiom __sum_def_3 {
(forall __ss1: Seq[Int], __ss2: Seq[Int] ::
{ (__sum(__ss1 ++ __ss2): Int) }
(__sum(__ss1 ++ __ss2): Int) ==
(__sum(__ss1): Int) + (__sum(__ss2): Int))
}
axiom __sum_def_4 {
(forall __ss1: Seq[Int], __ss2: Seq[Int] ::
{ (__sum(__ss1): Int), (__sum(__ss2): Int) }
(__toMS(__ss1): Multiset[Int]) == (__toMS(__ss2): Multiset[Int]) ==>
(__sum(__ss1): Int) == (__sum(__ss2): Int))
}
}
domain _list_ce_helper {
function seq_ref_length(___s: Seq[Ref]): Int
function seq_ref_index(___s: Seq[Ref], i: Int): Ref
axiom relate_length {
(forall ___s: Seq[Ref] :: { |___s| } |___s| == seq_ref_length(___s))
}
axiom relate_index {
(forall ___s: Seq[Ref], ___i: Int ::
{ ___s[___i] }
___s[___i] == seq_ref_index(___s, ___i))
}
}
domain Measure$ {
function Measure$create(guard: Bool, key: Ref, value: Int): Measure$
function Measure$guard(m: Measure$): Bool
function Measure$key(m: Measure$): Ref
function Measure$value(m: Measure$): Int
axiom Measure$A0 {
(forall g: Bool, k: Ref, v: Int ::
{ Measure$guard(Measure$create(g, k, v)) }
Measure$guard(Measure$create(g, k, v)) == g)
}
axiom Measure$A1 {
(forall g: Bool, k: Ref, v: Int ::
{ Measure$key(Measure$create(g, k, v)) }
Measure$key(Measure$create(g, k, v)) == k)
}
axiom Measure$A2 {
(forall g: Bool, k: Ref, v: Int ::
{ Measure$value(Measure$create(g, k, v)) }
Measure$value(Measure$create(g, k, v)) == v)
}
}
domain __MSHelper[T$] {
function __toMS(s: Seq[T$]): Multiset[T$]
axiom __toMS_def_1 {
(__toMS(Seq[T$]()): Multiset[T$]) == Multiset[T$]()
}
axiom __toMS_def_2 {
(forall __t: T$ ::
{ (__toMS(Seq(__t)): Multiset[T$]) }
(__toMS(Seq(__t)): Multiset[T$]) == Multiset(__t))
}
axiom __toMS_def_3 {
(forall __ss1: Seq[T$], __ss2: Seq[T$] ::
{ (__toMS(__ss1 ++ __ss2): Multiset[T$]) }
(__toMS(__ss1 ++ __ss2): Multiset[T$]) ==
((__toMS(__ss1): Multiset[T$]) union (__toMS(__ss2): Multiset[T$])))
}
axiom __toMS_def_4 {
(forall __ss1: Seq[T$] ::
{ (__toMS(__ss1): Multiset[T$]) }
|(__toMS(__ss1): Multiset[T$])| == |__ss1|)
}
}
domain _Name {
function _combine(n1: _Name, n2: _Name): _Name
function _single(n: Int): _Name
function _get_combined_prefix(n: _Name): _Name
function _get_combined_name(n: _Name): _Name
function _get_value(n: _Name): Int
function _name_type(n: _Name): Bool
function _is_single(n: _Name): Bool
function _is_combined(n: _Name): Bool
axiom decompose_single {
(forall i: Int :: { _single(i) } _get_value(_single(i)) == i)
}
axiom compose_single {
(forall n: _Name ::
{ _get_value(n) }
_is_single(n) ==> n == _single(_get_value(n)))
}
axiom type_of_single {
(forall i: Int :: { _single(i) } _name_type(_single(i)))
}
axiom decompose_combined {
(forall n1: _Name, n2: _Name ::
{ _combine(n1, n2) }
_get_combined_prefix(_combine(n1, n2)) == n1 &&
_get_combined_name(_combine(n1, n2)) == n2)
}
axiom compose_combined {
(forall n: _Name ::
{ _get_combined_prefix(n) }
{ _get_combined_name(n) }
_is_combined(n) ==>
n == _combine(_get_combined_prefix(n), _get_combined_name(n)))
}
axiom type_of_composed {
(forall n1: _Name, n2: _Name ::
{ _combine(n1, n2) }
!_name_type(_combine(n1, n2)))
}
axiom type_is_single {
(forall n: _Name :: { _name_type(n) } _name_type(n) == _is_single(n))
}
axiom type_is_combined {
(forall n: _Name ::
{ _name_type(n) }
!_name_type(n) == _is_combined(n))
}
}
domain IntWellFoundedOrder {
axiom integer_ax_dec {
(forall int1: Int, int2: Int ::
{ (decreasing(int1, int2): Bool) }
int1 < int2 ==> (decreasing(int1, int2): Bool))
}
axiom integer_ax_bound {
(forall int1: Int ::
{ (bounded(int1): Bool) }
int1 >= 0 ==> (bounded(int1): Bool))
}
}
domain PredicateInstancesWellFoundedOrder {
axiom predicate_instances_ax_dec {
(forall l1: PredicateInstance, l2: PredicateInstance ::
{ nestedPredicates(l1, l2) }
(decreasing(l1, l2): Bool) == nestedPredicates(l1, l2))
}
axiom predicate_instances_ax_bound {
(forall l1: PredicateInstance ::
{ (bounded(l1): Bool) }
(bounded(l1): Bool))
}
}
domain WellFoundedOrder[T] {
function decreasing(arg1: T, arg2: T): Bool
function bounded(arg1: T): Bool
}
domain PredicateInstancesNestedRelation {
function nestedPredicates(l1: PredicateInstance, l2: PredicateInstance): Bool
axiom nestedTrans {
(forall l1: PredicateInstance, l2: PredicateInstance, l3: PredicateInstance ::
{ nestedPredicates(l1, l2), nestedPredicates(l2, l3) }
nestedPredicates(l1, l2) && nestedPredicates(l2, l3) ==>
nestedPredicates(l1, l3))
}
axiom nestedReflex {
(forall l1: PredicateInstance ::!nestedPredicates(l1, l1))
}
}
domain PredicateInstance {
}
field _val: Ref
field __container: Ref
field __iter_index: Int
field __previous: Seq[Ref]
field list_acc: Seq[Ref]
field set_acc: Set[Ref]
field dict_acc: Map[Ref,Ref]
field Measure$acc: Seq[Ref]
field MustReleaseBounded: Int
field MustReleaseUnbounded: Int
field Node_function_name: Ref
field Node_children: Ref
function can_node_be_compressed(marked_execution_tree: Ref): Ref
requires issubtype(typeof(marked_execution_tree), Node())
requires acc(marked_execution_tree.Node_children, write) &&
issubtype(typeof(marked_execution_tree.Node_children), list(Node()))
requires acc(marked_execution_tree.Node_children.list_acc, write)
requires true &&
(forall lambda21_25$i: Ref ::
{ issubtype(typeof(lambda21_25$i), int()) }
issubtype(typeof(lambda21_25$i), int()) &&
issubtype(typeof(lambda21_25$i), int()) &&
(int___ge__(int___unbox__(lambda21_25$i), 0) &&
int___lt__(int___unbox__(lambda21_25$i), list___len__(marked_execution_tree.Node_children))) ==>
acc(list___getitem__(marked_execution_tree.Node_children, lambda21_25$i).Node_function_name, write)) &&
(forall lambda21_25$i: Ref ::
{ issubtype(typeof(lambda21_25$i), int()) }
issubtype(typeof(lambda21_25$i), int()) &&
issubtype(typeof(lambda21_25$i), int()) &&
(int___ge__(int___unbox__(lambda21_25$i), 0) &&
int___lt__(int___unbox__(lambda21_25$i), list___len__(marked_execution_tree.Node_children))) ==>
issubtype(typeof(list___getitem__(marked_execution_tree.Node_children,
lambda21_25$i).Node_function_name), str()))
requires acc(marked_execution_tree.Node_function_name, write) &&
issubtype(typeof(marked_execution_tree.Node_function_name), str())
ensures issubtype(typeof(result), int())
ensures !int___eq__(__prim__int___box__(list___len__(marked_execution_tree.Node_children)),
__prim__int___box__(1)) ==>
int___eq__(result, __prim__int___box__(0))
ensures int___eq__(result, __prim__int___box__(0))
{
(let cond_1 ==
(__prim__bool___box__(!int___eq__(__prim__int___box__(list___len__(marked_execution_tree.Node_children)),
__prim__int___box__(1)))) in
(true && bool___unbox__(cond_1) ?
__prim__int___box__(1) :
(let cond_0_0 ==
(__prim__bool___box__(!str___eq__(list___getitem__(marked_execution_tree.Node_children,
__prim__int___box__(0)).Node_function_name, marked_execution_tree.Node_function_name))) in
(true && bool___unbox__(cond_0_0) ?
__prim__int___box__(0) :
__prim__int___box__(int___add__(int___unbox__(can_node_be_compressed(list___getitem__(marked_execution_tree.Node_children,
__prim__int___box__(0)))), 1))))))
}
function __file__(): Ref
function __name__(): Ref
function __prim__int___box__(prim: Int): Ref
decreases _
ensures typeof(result) == int()
ensures int___unbox__(result) == prim
function int___unbox__(box: Ref): Int
decreases _
requires issubtype(typeof(box), int())
ensures !issubtype(typeof(box), bool()) ==>
__prim__int___box__(result) == box
ensures issubtype(typeof(box), bool()) ==>
__prim__bool___box__(result != 0) == box
function __prim__bool___box__(prim: Bool): Ref
decreases _
ensures typeof(result) == bool()
ensures bool___unbox__(result) == prim
ensures int___unbox__(result) == (prim ? 1 : 0)
function bool___unbox__(box: Ref): Bool
decreases _
requires issubtype(typeof(box), bool())
ensures __prim__bool___box__(result) == box
function int___eq__(self: Ref, other: Ref): Bool
decreases _
requires issubtype(typeof(self), int())
requires issubtype(typeof(other), int())
ensures result == (int___unbox__(self) == int___unbox__(other))
ensures result == object___eq__(self, other)
function int___ge__(self: Int, other: Int): Bool
decreases _
{
self >= other
}
function int___lt__(self: Int, other: Int): Bool
decreases _
{
self < other
}
function int___add__(self: Int, other: Int): Int
decreases _
{
self + other
}
function list___len__(self: Ref): Int
decreases _
requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
requires acc(self.list_acc, wildcard)
{
|self.list_acc|
}
function list___getitem__(self: Ref, key: Ref): Ref
decreases _
requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
requires issubtype(typeof(key), int())
requires acc(self.list_acc, wildcard)
requires (let ln ==
(list___len__(self)) in
(int___unbox__(key) < 0 ==> int___unbox__(key) >= -ln) &&
(int___unbox__(key) >= 0 ==> int___unbox__(key) < ln))
ensures result ==
(int___unbox__(key) >= 0 ?
self.list_acc[int___unbox__(key)] :
self.list_acc[list___len__(self) + int___unbox__(key)])
ensures issubtype(typeof(result), list_arg(typeof(self), 0))
function Level(r: Ref): Perm
decreases _
function str___len__(self: Ref): Int
decreases _
ensures result >= 0
function str___val__(self: Ref): Int
decreases _
function str___create__(len: Int, value: Int): Ref
decreases _
ensures str___len__(result) == len
ensures str___val__(result) == value
ensures typeof(result) == str()
function str___eq__(self: Ref, other: Ref): Bool
decreases _
requires issubtype(typeof(self), str())
ensures (str___val__(self) == str___val__(other)) == result
ensures result ==> str___len__(self) == str___len__(other)
ensures result == object___eq__(self, other)
predicate MustTerminate(r: Ref)
predicate MustInvokeBounded(r: Ref)
predicate MustInvokeUnbounded(r: Ref)
predicate _MaySet(rec: Ref, id: Int)