Skip to content

Commit bf5973a

Browse files
andreistefanescuclaude
andreistefanescu
and
claude
committed
feat: rename concat -> append_pure; add 6 vector pure variants; new InsertAtVec
vector_ext renames + new functions: - concat -> append_pure (matches std::vector::append; updates 5 test files that imported concat) - push_back_pure, pop_back_pure, push_front_pure, pop_front_pure, insert_pure, remove_pure — functional variants of std::vector ops (push_front/pop_front have no std counterpart) Boogie: - New InsertAtVec<T>(v, i, e) primitive in all three vector theories (vector-array, vector-array-intern, vector-smt-seq), parallel to RemoveAtVec. - vector_ext pure helpers use InsertAtVec / RemoveAtVec / InRangeVec consistently. - Fixed swapped argument order in $1_vector_insert{S}: Move signature is insert(v, e, i) but the Boogie procedure had (m, i, e) — corrected to (m, e, i). Was unused by any prior test, surfaced now by vector_ext::insert_pure's test_insert_matches. Tests: 7 *_pure tests for vector_ext, all verifying the functional helpers match the corresponding mutating ops via reference equality. All 436 tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 1a7a773 commit bf5973a

26 files changed

+356
-37
lines changed

‎crates/move-model/src/model.rs‎

Lines changed: 80 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1647,7 +1647,13 @@ impl GlobalEnv {
16471647
const PROVER_VEC_SUM: &'static str = "sum";
16481648
const PROVER_VEC_SUM_RANGE: &'static str = "sum_range";
16491649
const PROVER_VEC_SLICE: &'static str = "slice";
1650-
const PROVER_VEC_CONCAT: &'static str = "concat";
1650+
const PROVER_VEC_APPEND_PURE: &'static str = "append_pure";
1651+
const PROVER_VEC_PUSH_BACK_PURE: &'static str = "push_back_pure";
1652+
const PROVER_VEC_POP_BACK_PURE: &'static str = "pop_back_pure";
1653+
const PROVER_VEC_PUSH_FRONT_PURE: &'static str = "push_front_pure";
1654+
const PROVER_VEC_POP_FRONT_PURE: &'static str = "pop_front_pure";
1655+
const PROVER_VEC_INSERT_PURE: &'static str = "insert_pure";
1656+
const PROVER_VEC_REMOVE_PURE: &'static str = "remove_pure";
16511657

16521658
// vector function names
16531659
const VECTOR_REVERSE_FUNCTION_NAME: &'static str = "reverse";
@@ -2195,12 +2201,60 @@ impl GlobalEnv {
21952201
self.get_fun_qid_opt(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_VEC_SLICE)
21962202
}
21972203

2198-
pub fn prover_vec_concat_qid(&self) -> QualifiedId<FunId> {
2199-
self.get_fun_qid(Self::PROVER_VECTOR_EXT_MODULE_NAME, Self::PROVER_VEC_CONCAT)
2204+
pub fn prover_vec_append_pure_qid(&self) -> QualifiedId<FunId> {
2205+
self.get_fun_qid(
2206+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2207+
Self::PROVER_VEC_APPEND_PURE,
2208+
)
2209+
}
2210+
2211+
pub fn prover_vec_append_pure_qid_opt(&self) -> Option<QualifiedId<FunId>> {
2212+
self.get_fun_qid_opt(
2213+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2214+
Self::PROVER_VEC_APPEND_PURE,
2215+
)
2216+
}
2217+
2218+
pub fn prover_vec_push_back_pure_qid(&self) -> QualifiedId<FunId> {
2219+
self.get_fun_qid(
2220+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2221+
Self::PROVER_VEC_PUSH_BACK_PURE,
2222+
)
2223+
}
2224+
2225+
pub fn prover_vec_pop_back_pure_qid(&self) -> QualifiedId<FunId> {
2226+
self.get_fun_qid(
2227+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2228+
Self::PROVER_VEC_POP_BACK_PURE,
2229+
)
22002230
}
22012231

2202-
pub fn prover_vec_concat_qid_opt(&self) -> Option<QualifiedId<FunId>> {
2203-
self.get_fun_qid_opt(Self::PROVER_VECTOR_EXT_MODULE_NAME, Self::PROVER_VEC_CONCAT)
2232+
pub fn prover_vec_push_front_pure_qid(&self) -> QualifiedId<FunId> {
2233+
self.get_fun_qid(
2234+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2235+
Self::PROVER_VEC_PUSH_FRONT_PURE,
2236+
)
2237+
}
2238+
2239+
pub fn prover_vec_pop_front_pure_qid(&self) -> QualifiedId<FunId> {
2240+
self.get_fun_qid(
2241+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2242+
Self::PROVER_VEC_POP_FRONT_PURE,
2243+
)
2244+
}
2245+
2246+
pub fn prover_vec_insert_pure_qid(&self) -> QualifiedId<FunId> {
2247+
self.get_fun_qid(
2248+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2249+
Self::PROVER_VEC_INSERT_PURE,
2250+
)
2251+
}
2252+
2253+
pub fn prover_vec_remove_pure_qid(&self) -> QualifiedId<FunId> {
2254+
self.get_fun_qid(
2255+
Self::PROVER_VECTOR_EXT_MODULE_NAME,
2256+
Self::PROVER_VEC_REMOVE_PURE,
2257+
)
22042258
}
22052259

22062260
pub fn vector_module_id(&self) -> ModuleId {
@@ -3657,7 +3711,13 @@ impl GlobalEnv {
36573711
self.prover_vec_sum_qid(),
36583712
self.prover_vec_sum_range_qid(),
36593713
self.prover_vec_slice_qid(),
3660-
self.prover_vec_concat_qid(),
3714+
self.prover_vec_append_pure_qid(),
3715+
self.prover_vec_push_back_pure_qid(),
3716+
self.prover_vec_pop_back_pure_qid(),
3717+
self.prover_vec_push_front_pure_qid(),
3718+
self.prover_vec_pop_front_pure_qid(),
3719+
self.prover_vec_insert_pure_qid(),
3720+
self.prover_vec_remove_pure_qid(),
36613721
]);
36623722
}
36633723

@@ -3906,7 +3966,13 @@ impl GlobalEnv {
39063966
self.prover_vec_sum_qid(),
39073967
self.prover_vec_sum_range_qid(),
39083968
self.prover_vec_slice_qid(),
3909-
self.prover_vec_concat_qid(),
3969+
self.prover_vec_append_pure_qid(),
3970+
self.prover_vec_push_back_pure_qid(),
3971+
self.prover_vec_pop_back_pure_qid(),
3972+
self.prover_vec_push_front_pure_qid(),
3973+
self.prover_vec_pop_front_pure_qid(),
3974+
self.prover_vec_insert_pure_qid(),
3975+
self.prover_vec_remove_pure_qid(),
39103976
]);
39113977
}
39123978

@@ -4207,7 +4273,13 @@ impl GlobalEnv {
42074273
self.vec_map_get_idx_opt_qid(),
42084274
self.vec_map_keys_qid(),
42094275
self.prover_vec_slice_qid_opt(),
4210-
self.prover_vec_concat_qid_opt(),
4276+
self.prover_vec_append_pure_qid_opt(),
4277+
if self.has_prover_vector_module() { Some(self.prover_vec_push_back_pure_qid()) } else { None },
4278+
if self.has_prover_vector_module() { Some(self.prover_vec_pop_back_pure_qid()) } else { None },
4279+
if self.has_prover_vector_module() { Some(self.prover_vec_push_front_pure_qid()) } else { None },
4280+
if self.has_prover_vector_module() { Some(self.prover_vec_pop_front_pure_qid()) } else { None },
4281+
if self.has_prover_vector_module() { Some(self.prover_vec_insert_pure_qid()) } else { None },
4282+
if self.has_prover_vector_module() { Some(self.prover_vec_remove_pure_qid()) } else { None },
42114283
self.prover_vec_sum_qid_opt(),
42124284
self.prover_vec_sum_range_qid_opt(),
42134285
self.prover_range_qid_opt(),

‎crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl‎

Lines changed: 35 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ procedure {:inline 1} $1_vector_rotate_slice{{S}}(m: $Mutation (Vec ({{T}})), le
222222
n := left + (right - rot);
223223
}
224224

225-
procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), i: int, e: {{T}}) returns (m': $Mutation (Vec ({{T}}))) {
225+
procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), e: {{T}}, i: int) returns (m': $Mutation (Vec ({{T}}))) {
226226
var left_vec: Vec ({{T}});
227227
var right_vec: Vec ({{T}});
228228
var v: Vec ({{T}});
@@ -374,20 +374,50 @@ function {:inline} $0_vector_iter_slice{{S}}(v: Vec ({{T}}), start: int, end: in
374374
SliceVec(v, start, end)
375375
}
376376

377-
function {:inline} $0_vector_ext_concat{{S}}(v1: Vec ({{T}}), v2: Vec ({{T}})): Vec ({{T}}) {
377+
// prover::vector_ext::append_pure — functional concatenation.
378+
function {:inline} $0_vector_ext_append_pure{{S}}(v1: Vec ({{T}}), v2: Vec ({{T}})): Vec ({{T}}) {
378379
ConcatVec(v1, v2)
379380
}
380381

381-
// Total borrow: for in-range indices this is ReadVec(v, i); for out-of-range
382-
// indices the underlying vector theory returns an uninterpreted (but
383-
// deterministic) value — exactly the "unknown" semantics. Never aborts.
382+
// prover::vector_ext::borrow_or_unknown — total borrow. Out-of-range
383+
// returns an uninterpreted (but deterministic) value. Never aborts.
384384
procedure {:inline 1} $0_vector_ext_borrow_or_unknown{{S}}(v: Vec ({{T}}), i: int) returns (dst: {{T}}) {
385385
dst := ReadVec(v, i);
386386
}
387387
function {:inline} $0_vector_ext_borrow_or_unknown{{S}}$pure(v: Vec ({{T}}), i: int): {{T}} {
388388
ReadVec(v, i)
389389
}
390390

391+
// prover::vector_ext::push_back_pure
392+
function {:inline} $0_vector_ext_push_back_pure{{S}}(v: Vec ({{T}}), e: {{T}}): Vec ({{T}}) {
393+
ExtendVec(v, e)
394+
}
395+
396+
// prover::vector_ext::pop_back_pure — drop last; unchanged if empty.
397+
function {:inline} $0_vector_ext_pop_back_pure{{S}}(v: Vec ({{T}})): Vec ({{T}}) {
398+
(if LenVec(v) == 0 then v else SliceVec(v, 0, LenVec(v) - 1))
399+
}
400+
401+
// prover::vector_ext::push_front_pure
402+
function {:inline} $0_vector_ext_push_front_pure{{S}}(v: Vec ({{T}}), e: {{T}}): Vec ({{T}}) {
403+
InsertAtVec(v, 0, e)
404+
}
405+
406+
// prover::vector_ext::pop_front_pure — drop first; unchanged if empty.
407+
function {:inline} $0_vector_ext_pop_front_pure{{S}}(v: Vec ({{T}})): Vec ({{T}}) {
408+
(if LenVec(v) == 0 then v else RemoveAtVec(v, 0))
409+
}
410+
411+
// prover::vector_ext::insert_pure — insert at i; unchanged if i > length.
412+
function {:inline} $0_vector_ext_insert_pure{{S}}(v: Vec ({{T}}), e: {{T}}, i: int): Vec ({{T}}) {
413+
(if i > LenVec(v) then v else InsertAtVec(v, i, e))
414+
}
415+
416+
// prover::vector_ext::remove_pure — remove at i; unchanged if i out of range.
417+
function {:inline} $0_vector_ext_remove_pure{{S}}(v: Vec ({{T}}), i: int): Vec ({{T}}) {
418+
(if InRangeVec(v, i) then RemoveAtVec(v, i) else v)
419+
}
420+
391421
{%- if instance.is_number -%}
392422
{%- if include_vec_sum -%}
393423

‎crates/move-prover-boogie-backend/src/boogie_backend/prelude/vector-array-intern-theory.bpl‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,18 @@ function {:inline} RemoveAtVec<T>(v: Vec T, i: int): Vec T {
8787
l)))
8888
}
8989

90+
function {:inline} InsertAtVec<T>(v: Vec T, i: int, e: T): Vec T {
91+
(var l := v->l + 1;
92+
VecIntern(Vec(
93+
(lambda j: int ::
94+
if j >= 0 && j < l then
95+
if j < i then v->v[j]
96+
else if j == i then e
97+
else v->v[j-1]
98+
else DefaultVecElem()),
99+
l)))
100+
}
101+
90102
function {:inline} ConcatVec<T>(v1: Vec T, v2: Vec T): Vec T {
91103
(var l1, m1, l2, m2 := v1->l, v1->v, v2->l, v2->v;
92104
VecIntern(Vec(

‎crates/move-prover-boogie-backend/src/boogie_backend/prelude/vector-array-theory.bpl‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,18 @@ function {:inline} RemoveAtVec<T>(v: Vec T, i: int): Vec T {
6464
l))
6565
}
6666

67+
function {:inline} InsertAtVec<T>(v: Vec T, i: int, e: T): Vec T {
68+
(var l := v->l + 1;
69+
Vec(
70+
(lambda j: int ::
71+
if j >= 0 && j < l then
72+
if j < i then v->v[j]
73+
else if j == i then e
74+
else v->v[j-1]
75+
else DefaultVecElem()),
76+
l))
77+
}
78+
6779
function {:inline} ConcatVec<T>(v1: Vec T, v2: Vec T): Vec T {
6880
(var l1, m1, l2, m2 := v1->l, v1->v, v2->l, v2->v;
6981
Vec(

‎crates/move-prover-boogie-backend/src/boogie_backend/prelude/vector-smt-seq-theory.bpl‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,10 @@ function {:inline} RemoveAtVec<T>(v: Vec T, i: int): Vec T {
5353
ConcatVec(SliceVec(v, 0, i), SliceVec(v, i + 1, LenVec(v)))
5454
}
5555

56+
function {:inline} InsertAtVec<T>(v: Vec T, i: int, e: T): Vec T {
57+
ConcatVec3(SliceVec(v, 0, i), MakeVec1(e), SliceVec(v, i, LenVec(v)))
58+
}
59+
5660
function {:builtin "seq.++"} ConcatVec<T>(v1: Vec T, v2: Vec T): Vec T;
5761
/*private*/ function {:builtin "seq.++"} ConcatVec3<T>(v1: Vec T, v2: Vec T, v3: Vec T): Vec T;
5862
/*private*/ function {:builtin "seq.++"} ConcatVec4<T>(v1: Vec T, v2: Vec T, v3: Vec T, v4: Vec T): Vec T;

‎crates/sui-prover/tests/inputs/quantifiers/concat.ok.move‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// Tests for the prover::vector_ext::concat native. Also demonstrates using
1+
// Tests for the prover::vector_ext::append_pure native. Also demonstrates using
22
// concat in a loop invariant to express the relationship between the already-
33
// processed prefix and the unprocessed suffix of a source vector.
44

@@ -11,37 +11,37 @@ use prover::prover::{ensures, requires, invariant};
1111
#[spec_only]
1212
use prover::vector_iter::slice;
1313
#[spec_only]
14-
use prover::vector_ext::concat;
14+
use prover::vector_ext::append_pure;
1515

1616
// Concrete values: concat of two literal vectors.
1717
#[spec(prove)]
1818
fun test_concat_concrete() {
1919
let v1 = vector[1u64, 2, 3];
2020
let v2 = vector[4u64, 5];
21-
ensures(concat(&v1, &v2) == vector[1, 2, 3, 4, 5]);
21+
ensures(append_pure(&v1, &v2) == vector[1, 2, 3, 4, 5]);
2222
}
2323

2424
// Identity: concat with an empty vector on either side is the other vector.
2525
#[spec(prove)]
2626
fun test_concat_empty_left() {
2727
let empty: vector<u64> = vector[];
2828
let v = vector[1, 2, 3];
29-
ensures(concat(&empty, &v) == v);
29+
ensures(append_pure(&empty, &v) == v);
3030
}
3131

3232
#[spec(prove)]
3333
fun test_concat_empty_right() {
3434
let v = vector[1, 2, 3];
3535
let empty: vector<u64> = vector[];
36-
ensures(concat(&v, &empty) == v);
36+
ensures(append_pure(&v, &empty) == v);
3737
}
3838

3939
// Length additivity.
4040
#[spec(prove)]
4141
fun test_concat_length() {
4242
let v1 = vector[1u64, 2];
4343
let v2 = vector[3u64, 4, 5];
44-
let r = concat(&v1, &v2);
44+
let r = append_pure(&v1, &v2);
4545
ensures(vector::length(r) == vector::length(&v1) + vector::length(&v2));
4646
}
4747

@@ -52,7 +52,7 @@ fun test_concat_of_slices(v: &vector<u64>, i: u64) {
5252
requires(i <= vector::length(v));
5353
let prefix = slice(v, 0, i);
5454
let suffix = slice(v, i, vector::length(v));
55-
ensures(concat(prefix, suffix) == *v);
55+
ensures(append_pure(prefix, suffix) == *v);
5656
}
5757

5858
// Loop invariant expressed via concat: the vector built so far plus the
@@ -65,7 +65,7 @@ fun copy_vec(v: &vector<u64>): vector<u64> {
6565
invariant!(|| ensures(
6666
i <= n
6767
&& vector::length(&r) == i
68-
&& concat(&r, slice(v, i, n)) == *v
68+
&& append_pure(&r, slice(v, i, n)) == *v
6969
));
7070
while (i < n) {
7171
r.push_back(*vector::borrow(v, i));

‎crates/sui-prover/tests/inputs/quantifiers/filter_suffix_loop.ok.move‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
// Loop test with a suffix invariant for `filter`, expressed via concat. The
22
// invariant
33
//
4-
// concat(r, filter_range(v, i, n, p)) == filter(v, p)
4+
// append_pure(r, filter_range(v, i, n, p)) == filter(v, p)
55
//
66
// needs the start-step direction of filter's recursive axiom to verify.
77

88
module 0x42::filter_suffix_loop_ok;
99

1010
use prover::prover::{ensures, invariant};
1111
use prover::vector_iter::{filter, filter_range};
12-
use prover::vector_ext::concat;
12+
use prover::vector_ext::append_pure;
1313

1414
#[ext(pure)]
1515
fun is_odd(x: &u64): bool {
@@ -22,7 +22,7 @@ fun filter_odds(v: &vector<u64>): vector<u64> {
2222
let mut r = vector[];
2323
invariant!(|| ensures(
2424
i <= n
25-
&& concat(&r, filter_range!(v, i, n, |x| is_odd(x))) == *filter!(v, |x| is_odd(x))
25+
&& append_pure(&r, filter_range!(v, i, n, |x| is_odd(x))) == *filter!(v, |x| is_odd(x))
2626
));
2727
while (i < n) {
2828
if (is_odd(vector::borrow(v, i))) {

‎crates/sui-prover/tests/inputs/quantifiers/find_indices_suffix_loop.ok.move‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Loop test with a suffix invariant for `find_indices`, expressed via concat.
22
// The invariant
33
//
4-
// concat(r, find_indices_range(v, i, n, p)) == find_indices(v, p)
4+
// append_pure(r, find_indices_range(v, i, n, p)) == find_indices(v, p)
55
//
66
// needs the start-step direction of find_indices's recursive axiom to verify
77
// the loop body. find_indices uses compound-trigger recursive axioms so this
@@ -11,7 +11,7 @@ module 0x42::find_indices_suffix_loop_ok;
1111

1212
use prover::prover::{ensures, invariant};
1313
use prover::vector_iter::{find_indices, find_indices_range};
14-
use prover::vector_ext::concat;
14+
use prover::vector_ext::append_pure;
1515

1616
#[ext(pure)]
1717
fun is_odd(x: &u64): bool {
@@ -24,7 +24,7 @@ fun find_odd_indices(v: &vector<u64>): vector<u64> {
2424
let mut r = vector[];
2525
invariant!(|| ensures(
2626
i <= n
27-
&& concat(&r, find_indices_range!(v, i, n, |x| is_odd(x)))
27+
&& append_pure(&r, find_indices_range!(v, i, n, |x| is_odd(x)))
2828
== *find_indices!(v, |x| is_odd(x))
2929
));
3030
while (i < n) {

‎crates/sui-prover/tests/inputs/quantifiers/map_suffix_loop.ok.move‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
// Loop test with a suffix invariant for `map`, expressed via concat. The
22
// invariant
33
//
4-
// concat(r, map_range(v, i, n)) == map(v, f)
4+
// append_pure(r, map_range(v, i, n)) == map(v, f)
55
//
66
// needs the start-step direction of map's recursive axiom to verify the body.
77

88
module 0x42::map_suffix_loop_ok;
99

1010
use prover::prover::{ensures, invariant};
1111
use prover::vector_iter::{map, map_range};
12-
use prover::vector_ext::concat;
12+
use prover::vector_ext::append_pure;
1313

1414
#[ext(pure)]
1515
fun double(x: &u64): u64 {
@@ -26,7 +26,7 @@ fun map_doubles(v: &vector<u64>): vector<u64> {
2626
let mut r = vector[];
2727
invariant!(|| ensures(
2828
i <= n
29-
&& concat(&r, map_range!(v, i, n, |x| double(x))) == *map!(v, |x| double(x))
29+
&& append_pure(&r, map_range!(v, i, n, |x| double(x))) == *map!(v, |x| double(x))
3030
));
3131
while (i < n) {
3232
r.push_back(double(vector::borrow(v, i)));

0 commit comments

Comments
 (0)