From b47a790878985d7c707ee7027e2cc9f635fde11d Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Mon, 27 Apr 2026 01:52:14 -0700 Subject: [PATCH] more nla spec --- .../datastructures/big_ordered_map.spec.move | 245 +++++++++++++++--- .../sources/transaction_context.spec.move | 8 + .../aptos-stdlib/sources/math64.move | 3 + .../aptos-stdlib/sources/math_fixed.spec.move | 2 + .../framework/cached-packages/src/head.mrb | Bin 1371951 -> 1371998 bytes .../move-stdlib/sources/string.spec.move | 6 + .../boogie-backend/src/prelude/native.bpl | 37 +++ 7 files changed, 266 insertions(+), 35 deletions(-) diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move index fd40cee0fb6..353a17d7fe8 100644 --- a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move +++ b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move @@ -26,6 +26,12 @@ spec aptos_framework::big_ordered_map { spec new_with_config { pragma verify = false; pragma opaque; + aborts_if inner_max_degree != 0 + && (inner_max_degree < 4 || (inner_max_degree as u64) > 4096); + aborts_if leaf_max_degree != 0 + && (leaf_max_degree < 3 || (leaf_max_degree as u64) > 4096); + ensures spec_len(result) == 0; + ensures forall k: K: !spec_contains_key(result, k); } spec new { @@ -35,11 +41,17 @@ spec aptos_framework::big_ordered_map { spec new_with_reusable { pragma verify = false; pragma opaque; + aborts_if false; + ensures spec_len(result) == 0; + ensures forall k: K: !spec_contains_key(result, k); } spec new_with_type_size_hints { pragma verify = false; pragma opaque; + aborts_if false; + ensures spec_len(result) == 0; + ensures forall k: K: !spec_contains_key(result, k); } spec borrow { @@ -65,12 +77,43 @@ spec aptos_framework::big_ordered_map { spec remove { pragma opaque; pragma verify = false; - aborts_if [abstract] !spec_contains_key(self, key); - ensures [abstract] !spec_contains_key(self, key); - ensures [abstract] spec_get(old(self), key) == result; - ensures [abstract] spec_len(old(self)) == spec_len(self) + 1; - ensures [abstract] forall k: K where k != key: spec_contains_key(self, k) ==> spec_get(self, k) == spec_get(old(self), k); - ensures [abstract] forall k: K where k != key: spec_contains_key(old(self), k) == spec_contains_key(self, k); + aborts_if !spec_contains_key(self, key); + ensures !spec_contains_key(self, key); + ensures spec_get(old(self), key) == result; + ensures spec_len(old(self)) == spec_len(self) + 1; + ensures spec_unchanged_except_at(self, old(self), key); + // ensures forall k: K where k != key: spec_contains_key(self, k) ==> spec_get(self, k) == spec_get(old(self), k); + // ensures forall k: K where k != key: spec_contains_key(old(self), k) == spec_contains_key(self, k); + } + + spec fun spec_unchanged_except_at( + new_map: BigOrderedMap, old_map: BigOrderedMap, key: &K + ): bool { + (forall k: K where k != key: + spec_contains_key(new_map, k) == spec_contains_key(old_map, k)) + && (forall k: K where k != key && spec_contains_key(old_map, k): + spec_get(new_map, k) == spec_get(old_map, k)) + } + + spec remove_or_none( + self: &mut BigOrderedMap, key: &K + ): Option { + pragma opaque; + pragma verify = false; + aborts_if false; + // Hit: key was present + ensures spec_contains_key(old(self), key) ==> ( + option::is_some(result) + && option::spec_borrow(result) == spec_get(old(self), key) + && !spec_contains_key(self, key) + && spec_len(self) == spec_len(old(self)) - 1 + ); + // Miss: key was absent — map unchanged + ensures !spec_contains_key(old(self), key) ==> ( + option::is_none(result) + && spec_len(self) == spec_len(old(self)) + ); + ensures spec_unchanged_except_at(self, old(self), key); } spec is_empty { @@ -80,31 +123,63 @@ spec aptos_framework::big_ordered_map { spec iter_is_end { pragma opaque; pragma verify = false; + aborts_if false; + ensures result == (self is IteratorPtr::End); } spec iter_borrow { pragma opaque; pragma verify = false; + aborts_if iter_is_end(self, map); + ensures result == spec_get(map, self.key); } + // Body also asserts constant_kv_size OR bcs::constant_serialized_size().is_some() + // which is not expressible from spec context. Caller-side, iter_is_end is what's discharged. spec iter_borrow_mut { pragma opaque; pragma verify = false; + aborts_if iter_is_end(self, map); + ensures result == spec_get(map, self.key); } spec iter_is_begin { pragma opaque; pragma verify = false; - } - + aborts_if false; + // self is End: returns true iff map is empty (End acts as both begin and end on []). + ensures (self is IteratorPtr::End) ==> (result <==> spec_len(map) == 0); + // self is Some: returns true iff self.key is the smallest key currently in map. + ensures !(self is IteratorPtr::End) ==> (result <==> + (spec_contains_key(map, self.key) + && (forall k: K where spec_contains_key(map, k) && k != self.key: + std::cmp::compare(self.key, k) == std::cmp::Ordering::Less))); + } + + // Returns the iterator pointing to the smallest key K in self with K >= input + // key (compare not Less), or End if no such key exists. spec internal_lower_bound { pragma opaque; pragma verify = false; + aborts_if false; + // End iff no key >= input exists (all keys are Less than input). + ensures iter_is_end(result, self) <==> + (forall k: K where spec_contains_key(self, k): + std::cmp::compare(k, key) == std::cmp::Ordering::Less); + // Otherwise, result.key is in the map, >= input, and the smallest such. + ensures !iter_is_end(result, self) ==> spec_contains_key(self, result.key); + ensures !iter_is_end(result, self) ==> + std::cmp::compare(result.key, key) != std::cmp::Ordering::Less; + ensures !iter_is_end(result, self) ==> + (forall k: K where spec_contains_key(self, k) && std::cmp::compare(k, key) != std::cmp::Ordering::Less: + std::cmp::compare(result.key, k) != std::cmp::Ordering::Greater); } spec iter_borrow_key { pragma opaque; pragma verify = false; + aborts_if self is IteratorPtr::End; + ensures result == self.key; } spec allocate_spare_slots { @@ -130,32 +205,30 @@ spec aptos_framework::big_ordered_map { spec keys { pragma verify = false; pragma opaque; - ensures [abstract] forall k: K: vector::spec_contains(result, k) <==> spec_contains_key(self, k); + ensures forall k: K: vector::spec_contains(result, k) <==> spec_contains_key(self, k); } spec new_from(keys: vector, values: vector): BigOrderedMap { pragma opaque; pragma verify = false; - aborts_if [abstract] exists i in 0..len(keys), j in 0..len(keys) where i != j : keys[i] == keys[j]; - aborts_if [abstract] len(keys) != len(values); - ensures [abstract] forall k: K {spec_contains_key(result, k)} : vector::spec_contains(keys,k) <==> spec_contains_key(result, k); - ensures [abstract] forall i in 0..len(keys) : spec_get(result, keys[i]) == values[i]; - ensures [abstract] spec_len(result) == len(keys); + aborts_if exists i in 0..len(keys), j in 0..len(keys) where i != j : keys[i] == keys[j]; + aborts_if len(keys) != len(values); + ensures forall k: K {spec_contains_key(result, k)} : vector::spec_contains(keys,k) <==> spec_contains_key(result, k); + ensures forall i in 0..len(keys) : spec_get(result, keys[i]) == values[i]; + ensures spec_len(result) == len(keys); } spec upsert { pragma opaque; pragma verify = false; - ensures [abstract] !spec_contains_key(old(self), key) ==> option::is_none(result); - ensures [abstract] spec_contains_key(self, key); - ensures [abstract] spec_get(self, key) == value; - ensures [abstract] spec_contains_key(old(self), key) ==> ((option::is_some(result)) && (option::spec_borrow(result) == spec_get(old( + ensures !spec_contains_key(old(self), key) ==> option::is_none(result); + ensures spec_contains_key(self, key); + ensures spec_get(self, key) == value; + ensures spec_contains_key(old(self), key) ==> ((option::is_some(result)) && (option::spec_borrow(result) == spec_get(old( self), key))); - ensures [abstract] !spec_contains_key(old(self), key) ==> spec_len(old(self)) + 1 == spec_len(self); - ensures [abstract] spec_contains_key(old(self), key) ==> spec_len(old(self)) == spec_len(self); - ensures [abstract] forall k: K: spec_contains_key(old(self), k) && k != key ==> spec_get(old(self), k) == spec_get(self, k); - ensures [abstract] forall k: K: spec_contains_key(old(self), k) ==> spec_contains_key(self, k); - ensures [abstract] forall k: K: spec_contains_key(self, k) ==> (k == key || spec_contains_key(old(self), k)); + ensures !spec_contains_key(old(self), key) ==> spec_len(old(self)) + 1 == spec_len(self); + ensures spec_contains_key(old(self), key) ==> spec_len(old(self)) == spec_len(self); + ensures spec_unchanged_except_at(self, old(self), key); } spec add_all { @@ -166,38 +239,70 @@ spec aptos_framework::big_ordered_map { spec borrow_front(self: &BigOrderedMap): (K, &V) { pragma opaque; pragma verify = false; - ensures [abstract] spec_contains_key(self, result_1); - ensures [abstract] spec_get(self, result_1) == result_2; - ensures [abstract] forall k: K where k != result_1: spec_contains_key(self, k) ==> + ensures spec_contains_key(self, result_1); + ensures spec_get(self, result_1) == result_2; + ensures forall k: K where k != result_1: spec_contains_key(self, k) ==> std::cmp::compare(result_1, k) == std::cmp::Ordering::Less; } + spec front_key(self: &BigOrderedMap): K { + pragma opaque; + pragma verify = false; + aborts_if spec_len(self) == 0; + ensures spec_contains_key(self, result); + ensures forall k: K where k != result: spec_contains_key(self, k) ==> + std::cmp::compare(result, k) == std::cmp::Ordering::Less; + } + spec borrow_back { pragma opaque; pragma verify = false; - ensures [abstract] spec_contains_key(self, result_1); - ensures [abstract] spec_get(self, result_1) == result_2; - ensures [abstract] forall k: K where k != result_1: spec_contains_key(self, k) ==> + ensures spec_contains_key(self, result_1); + ensures spec_get(self, result_1) == result_2; + ensures forall k: K where k != result_1: spec_contains_key(self, k) ==> std::cmp::compare(result_1, k) == std::cmp::Ordering::Greater; } + spec back_key(self: &BigOrderedMap): K { + pragma opaque; + pragma verify = false; + aborts_if spec_len(self) == 0; + ensures spec_contains_key(self, result); + ensures forall k: K where k != result: spec_contains_key(self, k) ==> + std::cmp::compare(result, k) == std::cmp::Ordering::Greater; + } + spec pop_front(self: &mut BigOrderedMap): (K, V) { pragma opaque; pragma verify = false; + ensures spec_contains_key(old(self), result_1); + ensures result_2 == spec_get(old(self), result_1); + ensures !spec_contains_key(self, result_1); + ensures spec_len(self) == spec_len(old(self)) - 1; + ensures spec_unchanged_except_at(self, old(self), result_1); + ensures forall k: K where spec_contains_key(old(self), k) && k != result_1: + std::cmp::compare(result_1, k) == std::cmp::Ordering::Less; } - spec pop_back { + spec pop_back(self: &mut BigOrderedMap): (K, V) { pragma opaque; pragma verify = false; + ensures spec_contains_key(old(self), result_1); + ensures result_2 == spec_get(old(self), result_1); + ensures !spec_contains_key(self, result_1); + ensures spec_len(self) == spec_len(old(self)) - 1; + ensures spec_unchanged_except_at(self, old(self), result_1); + ensures forall k: K where spec_contains_key(old(self), k) && k != result_1: + std::cmp::compare(result_1, k) == std::cmp::Ordering::Greater; } spec prev_key(self: &BigOrderedMap, key: &K): Option { pragma opaque; pragma verify = false; - ensures [abstract] result == std::option::spec_none() <==> + ensures result == std::option::spec_none() <==> (forall k: K {spec_contains_key(self, k)} where spec_contains_key(self, k) && k != key: std::cmp::compare(key, k) == std::cmp::Ordering::Less); - ensures [abstract] result.is_some() <==> + ensures result.is_some() <==> spec_contains_key(self, option::spec_borrow(result)) && (std::cmp::compare(option::spec_borrow(result), key) == std::cmp::Ordering::Less) && (forall k: K {spec_contains_key(self, k), std::cmp::compare(option::spec_borrow(result), k), std::cmp::compare(key, k)} where k != option::spec_borrow(result): ((spec_contains_key(self, k) && @@ -209,10 +314,10 @@ spec aptos_framework::big_ordered_map { spec next_key(self: &BigOrderedMap, key: &K): Option { pragma opaque; pragma verify = false; - ensures [abstract] result == std::option::spec_none() <==> + ensures result == std::option::spec_none() <==> (forall k: K {spec_contains_key(self, k)} where spec_contains_key(self, k) && k != key: std::cmp::compare(key, k) == std::cmp::Ordering::Greater); - ensures [abstract] result.is_some() <==> + ensures result.is_some() <==> spec_contains_key(self, option::spec_borrow(result)) && (std::cmp::compare(option::spec_borrow(result), key) == std::cmp::Ordering::Greater) && (forall k: K {spec_contains_key(self, k)} where k != option::spec_borrow(result): ((spec_contains_key(self, k) && @@ -224,36 +329,106 @@ spec aptos_framework::big_ordered_map { spec internal_find { pragma opaque; pragma verify = false; + aborts_if false; + ensures iter_is_end(result, self) <==> !spec_contains_key(self, key); + ensures !iter_is_end(result, self) ==> result.key == key; } spec internal_new_begin_iter { pragma opaque; pragma verify = false; + aborts_if false; + ensures iter_is_end(result, self) <==> spec_len(self) == 0; + ensures !iter_is_end(result, self) ==> spec_contains_key(self, result.key); + // result.key is the smallest key in the map. + ensures !iter_is_end(result, self) ==> + (forall k: K where spec_contains_key(self, k) && k != result.key: + std::cmp::compare(result.key, k) == std::cmp::Ordering::Less); } spec internal_new_end_iter { pragma opaque; pragma verify = false; + aborts_if false; + ensures result is IteratorPtr::End; } spec iter_next { pragma opaque; pragma verify = false; + aborts_if iter_is_end(self, map); } spec iter_prev { pragma opaque; pragma verify = false; + aborts_if iter_is_begin(self, map); } spec compute_length { pragma verify = false; pragma opaque; - ensures [abstract] result == spec_len(self); + ensures result == spec_len(self); } spec iter_modify { pragma opaque; pragma verify = false; + aborts_if iter_is_end(self, map); + // iter_modify mutates the value at self.key via the closure. Containment is + // unchanged for every key; values for keys other than self.key are preserved. + ensures spec_contains_key(map, self.key); + ensures spec_len(map) == spec_len(old(map)); + ensures spec_unchanged_except_at(map, old(map), self.key); + } + + spec internal_find_with_path { + pragma opaque; + pragma verify = false; + aborts_if false; + ensures iter_is_end(result.iterator, self) <==> !spec_contains_key(self, key); + ensures !iter_is_end(result.iterator, self) ==> result.iterator.key == key; + } + + spec iter_with_path_get_iter { + pragma opaque; + pragma verify = false; + aborts_if false; + ensures result == self.iterator; + } + + spec iter_remove { + pragma opaque; + pragma verify = false; + aborts_if iter_is_end(self.iterator, map); + ensures result == spec_get(old(map), self.iterator.key); + ensures !spec_contains_key(map, self.iterator.key); + ensures spec_len(map) == spec_len(old(map)) - 1; + ensures spec_unchanged_except_at(map, old(map), self.iterator.key); + } + + spec internal_leaf_new_begin_iter { + pragma opaque; + pragma verify = false; + aborts_if false; + } + + spec internal_leaf_iter_is_end { + pragma opaque; + pragma verify = false; + aborts_if false; + } + + spec internal_leaf_borrow_value { + pragma opaque; + pragma verify = false; + aborts_if false; + ensures result == self.value; + } + + spec internal_leaf_iter_borrow_entries_and_next_leaf_index { + pragma opaque; + pragma verify = false; + aborts_if internal_leaf_iter_is_end(self); } } diff --git a/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move b/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move index 79869d5d7e7..326184e191d 100644 --- a/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move +++ b/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move @@ -116,10 +116,18 @@ spec aptos_framework::transaction_context { spec monotonically_increasing_counter_internal(timestamp_us: u64): u128 { //TODO: temporary mockup pragma opaque; + aborts_if [abstract] false; } spec monotonically_increasing_counter_internal_for_test_only(): u128 { //TODO: temporary mockup pragma opaque; + aborts_if [abstract] false; + } + + spec monotonically_increasing_counter(): u128 { + pragma opaque; + // Assume that the monotonically increasing counter is always increasing. + aborts_if [abstract] false; } } diff --git a/aptos-move/framework/aptos-stdlib/sources/math64.move b/aptos-move/framework/aptos-stdlib/sources/math64.move index 9b89acbe809..3043ea35e1e 100644 --- a/aptos-move/framework/aptos-stdlib/sources/math64.move +++ b/aptos-move/framework/aptos-stdlib/sources/math64.move @@ -87,6 +87,9 @@ module aptos_std::math64 { res += n; }; n >>= 1; + } spec { + invariant (res as u64) + 2 * (n as u64) <= 64; + invariant n == 0 ==> (res as u64) <= 63; }; res } diff --git a/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move b/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move index 1442eb30553..bff9f0dbf9e 100644 --- a/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move +++ b/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move @@ -4,6 +4,8 @@ spec aptos_std::math_fixed { /// No loop in the body, so callers can inline without havocing. spec sqrt(x: FixedPoint32): FixedPoint32 { aborts_if false; + // Zero input → zero output, directly from math128::sqrt's ensures. + ensures x.get_raw_value() == 0 ==> result.get_raw_value() == 0; } /// `mul_div` aborts when z is zero or when x * y / z overflows u64. diff --git a/aptos-move/framework/cached-packages/src/head.mrb b/aptos-move/framework/cached-packages/src/head.mrb index c93fc27c2457882d331817e917779ef4893e3f63..c767e605a65bc6822d03154c0a8843174c0813cc 100644 GIT binary patch delta 3500 zcmYk~&NOs|D`sVhK%eaw|$S9pkR>s#zE~|7hGfGz1GP5ZoLe$qD zg={CB&9_LD5oi3a?_a<7GWpZC9?cL~Rm!?AoMu7{jj`1f1rf!?Du@qOKNhnTEds}r_54EAH^47O$@y$)nBQbT0Y+1&6puSr7bN|n^k?*gX?I`+%MaZ0NZhbHek0wpT zlBA*^NKmhqie8nUt`uWh##_|+hgna*o*gWDKxZm_5L?Dw=*7fHR8>_3vnA~8-i!V= zfvf*s?;GuCVHDNL`z?)*R;~T|u{~T3xLMr0RzGPsCU0K0GWhZOx#L%K6B=jNYam%R zb%C3|{$bwPUoPpF)7`@abN8B};`=w{?v{H~`6E>tHRQQ!GfD%ZTVB

{pNBcP-$C zI5bm=b`kc@^!f+9#3!W?x?kj{{C5tm`~H~e5||N_VM>#2>HS(s+`H_f5cjlN%lTFVm5Rn=AJjU3J6B$je;QfIKY!WHmbiPgU? zi>5}GwN~Eil@AncWtlqIwKiV!|LQ(-Ytp))H=5b>y^nb!2f1jl=ksCH?fcXV$vV?J zc#-+CA#h;b2)|-eoJnlZD1}@2JM$n#%M{#ZKee^ezPN7uKyQqc&q(@RR<-VIl$STa zod1kpAbu1;#ZKG}Yf#1ZJ@2|Y-H2!F6;BQq_~U;Yh5yCZ^tQ%EJ;rWT+o}VS&{bYS zEpEmo$D{5mn4D;Oa5>9l)td9`p<&Pcx8?(v6bz$l9y*k9 z?FwE#mT4BbtPE!g3j{zm;SUO<57w1|nc0^SdLNYYrf3PUnICb)Q`Q%w%%vhV>fW#O zHye5*Bj%EXov_=fp=YE)#r*HG5BI4*^w=v>4MA`Rr&Qbhrwx~z$NcfOHS(3BNyQeA z#M3j3rTnPn;~!Uim3vljjx3D?`+gUWd5Kj_WZl@@qZbzJTiU_^vph((ue`x9GZvF) z`$c^gX&K-tpf2;Xg8Ye&fBS6wN%!vyE?Luy7@Q$RWKnYF9_LV_%CpMDC&B_qA`R8$ z8<&HXsowCVZ`=$}ORt}~h(7mglY&L&REdY;o3r{Yb%Y#BnshqmPOz9OdEj`@O7-;D zT3?-Ain{q4^9J{NO)`NM-#77wneJgd+l!p*ygwlmkuMooRBszZs15)*qP0#Ur9({H zUQ@RDhKhd+UAlSZXsCU3?I{t)x3~i#T)Ii3@yRbRv6bb}C{nDe=0aPXo_*#SxKucn zG}+#QqlU^eeefbpd%v59^n}(sWw?_zwpiw9hS0GOl`TI&dJpZ*m&Spc+Y6Wn&U+$9s1F#fyG;bU z$o5vlY0yYQVMU*@NpU8V^ulFA0ZTa3OZ^c?$w)&9>~7a7A-O1|GW=BN+=a$vLUI_6tI;!nut8@4I0z;~>3&Tjy)vlChJzh#n z7x=C!(Rp^ksx^X-;k6YWQ|f5LsPC=D`yn7I^Od6r|43hjEC z6cQ8Fl$K60zwu?N<5>R71W#oeA+} zx4jD~@0Zx5W|=U*9TtZ+?9Bgr`|D$P7s_b)&>Tt})ouW6&&};F6SeyH)sRnu)A&Qp zRj&?*;uHgUKCT8pT8r|`r)t#vyH3UDzF6|HQnLaUyij}?7i&P zz4I)O6QQg!@+-_#ge*yLg2D-TaB1faW03EN`c!aK;|sHFu~R-6Tt!z`}E(%}#zFIlYZjbJWZ%(Cg{k8si;7(J}Fra%fif0@4Zx3H6cG=WgW{y3Sp5HM#bo}7v+oZ4APMxJsE3(^}nww#= zz4ad1LmCR#K;NH$daA}$2k0aK}CCvQfIZ57>d zVm{i^*L~0?jevjhYHD_PZzC$^lh;x|{nUZ*z=7}cmIHf2p60jDut}>4g zg7tv$!ZUAv4m;(+m;DA@98k8%U=tmqLZ&h!sD?E`d6~f|WV}fYS<2lfl=k{w%6NAy zY&ipV<=A>gruCFT*G%`ao3s9+{yo050?Hy4ulq_;| zf6E~09`H%hu~c{lt;~QL`<}^NfTq_h@2d{}5Yl#W4bUDnW2R(kxM}x;=Z3ryOpble zEsxXQWiz%hea+Zog$}|JQv-^3UU{xUW<;MH@9|LEvBQaN=IGt>aThm=&8dX%b_Bv? zgQVxfZnsnvbW~@tv?iB4=1{v6fSYI=?kG?+eW`e93LrEBpN7;8W?^8i4`f9ZuAfg;rG)zN=UnUw6lw^SeVt zVvW7-Kd$IBl%*ljMbde!&`xoJzJ5P{c%#e1NTK& zy1HU-pcb_nY*z~lAUnGY%$<$c*Ov|+xj^#N3Wwu&-J4?fWqVKfKmENEd?1*cQeux< zoKaD3dwMsdadX4>XjX2tWsj3d?CIe7=C%`ZAukB_$;sF7q>*`{D+;}bFMWQedC}7! zQ+9g&{IJ&@#^NavuFo83eYVZE{!MQrlCevl%{v)7KPTh-i*(exZeRG^Qp`}`-F4lu zDX;I`sQi6ERsKHzhBcs{m2M4G0ylwpKXWiZh&6T&h^gAQ2EGL-sw4Se00`fo&VL0L zP({ka_|+i%NIoS2WnKrsGCmK~RTFZ9@RGbVKLqf9X%}7^s0IQ4NvrZY09M0!Am;FY z2>|a!6@hC|K8OJ8o(=FMz=l<71C+xV30gwHumeyb=mBw<5EO(2AYdRU_|E|r)P@RR zkn&nkA#o89Ka>wC4-t^if(Z(uS%Q~KuCk*8KYh~E$DlA|8i9tvppi5T5rZO-aVR7OgQU?gyyXRj!=Vuvsy>BAKoF5w z44yzn5ox^r2SY%TaWoV;%3Vc(N00}^Bg6ydIlu$qf%3q3gn16~9O605Bf=xfbEL{$ IMXaU$e_(Z4kpKVy delta 3474 zcmYk9c{CL69>y_aX~vptjcjSMo6Rf|&6t^NCB|gUmJuRLlC9>4B3ne7M3xZQvQHrq z5hW6mWl-7I>{;)0&pr3v_ngoB{_%XD^ZfJu<9%2x%1ag{QTz;KNDL-o zae%ov!07{_e-xLE<>UB!xDMXicqI%P9Ny1x_)^rzO63RC1f@wu8Wh#Jh$%C16D(b# zRNEOqzZ7PUAvNH+zjK=E1%W`)qBp7xa^Q=z!9j(!wY5)fzt!9qscY&HU^vgULLRha zEWOW&Yw3?w(6j<;3jZd@ynS(2nf1C!+xJ_=Cf&K{QMBgWx>)Kj;_sEk`_B`iete9T z;L21?3U_!}|He-H)CBkM#)i5OeTRe6x91>A`A^Qtg7)7FaEXB(O1%1ieOVV(Hj!~C zkc)Xg$J9I6X}jrtFuS`oesZd_ZgWWwyTm$h8I1;lI`2>&H}I{71?np!KI(AW65?(y zF_G>$g@_9_sWqN#UZ(0i9s6d} z^re4&&sZ^}iI%jad1PLbx!Ge=@g4bL zzSAMaKW-a3hDCH%p$hUl{flE{XARc6;{v658)RgI>ScQQ-i;j39coE<^HkILaRxo2 z)4@{{{7}kM{Oul3RF_9FCM~Ch12x@)D{;qV)3(S9_wv%;HL z+@kR?0dddCSgpClE|^a>?3Z|H=(>NamE2FcvGe?kF{C%+-IHFrK_Vdr=FZubR`dIo zv&9oUzIQG}E7=1$pT3JQsPuRy>a9lSQf8PWnzqwknJG4Jox0qF@9R^xh|C5pE!K13 zdTh0qLo4oyX4F6CygETGRO{tIR#u9o5O|3rS84-vRZK^_S zRBs!_?3)bqZQ=!DlV=hY!Z-S&NV$Y&havK0Dp!lnbT>IeJ5#s;XILfgAta|$Lfqa@ zGSH)dj{KAzY_Km;?4QV46OyK%JS7%XWfF9yWwV5EF|Pi`Sc#6BosNF_YYD~?fvm~K zQkQKGR&fh&ke{hoxKs2_h=~7e`k`>k>I_AL(n0AX%brC6LL3nl&G#W3r*eM0s7Qz* z4Mj8E+F#P9=Z9fDG9)2}{DJk|fx3E!6Q5cXcHM5=9m)QY^ij8oCObAyPkANV*z=+M z@-)wevOf?~5EEl3YQ35?EQ$nd*fBhnK6k8)RpowF@t2t3$YUDMw3UAFuTn9~ZkyYn zI|AyngrJ*Vd%KRAN%MzP1Z>>ziD)}|$!G(c$6S2pQXla3Qd%7caCsb!Pu`r%3D)bN z5>m-s%V!QO(74G)yjMOwBh2flEK$`~=We*RnrSl?;HT?i`dI+1aga_es5w8ai_@;W ztg8Cw^vKH!>}zM5_LLuW&G<*8`5hx)<%T75ud+sTSaH^>)ta&7w-boH{at9eDJJ@Y zH)*on=uA_Sb(^UIN4iYeFPR?SU*>qzdgHIgwdsLc(I=JBN?(w4htoj5NZ#YGDzsk$ z@B26=P1`gHC=8C*XDOxdpiAG@UOe?`^A$xjwqeA{{u950{dx=JVZX&myub&N;1Sb; zXNKNHQAgd+m(@4|wtrB~rei>B6Xss4$!wyOR+jkm@F=q&Hi%RRG=)gmTjRqe zWm5VclqB;=hqUlNaM!ato-k$Xs9^>{1o1DUI~+D*Ao3?nSQohSP&)4X`E))3vFgB) z&bHXsg~5W>bOTdaV#VMepA8N_#f2VL;^bk#iy06uHKKx!@Cgl~D!DZkVcoM2)0LlH zIvlJLov2)yLop@BTm-$(xb`v;3^!0NL7%#~(R8qr{le&`VzqsU%d@IiUV_2oC7He($vwbT7k-^WyOm3PEK%q-=Y_wiY zU7%pH1!=+F0A?B#5OwtOYEfKpQU$^y}-`9+#X|fBm?ynv~DE^7i5J z+e{C-UWZitC$f8qc(`ltXLn%zf_!p3q?@a+ASFhwGs`2qDgDBGoto61YcNh!i?1_P z=?1L7Rbjn**7*U88Kj(7KIm2q-m+5Hbv~M$SRHwE(01r(X8s8!s5V6af<3>*H$b2+ zU&%3vCG4ZuryYA;_)?2-Hu^<|cu>6mh&BD(a%vE(tdpmf(?{y+R;#*s3BGVN%TPo9 zv02acobX4djTn!=bDghke;grRrS27X1BrrM_uk8hG8&W;GX9;}U+1Quqm~UF{Uj-;B8fq(2(l`%meBwB7N^WwW%mP`VFzRQ!kK1`3(bWJ{MXNMK%R8;Fl(y=rA8=0P zYZlEz+S|q#rJ4!V6ANNiHY6s0@0hV&F*H}t{#sYPt02iek)?u3JJfM)yDd6C<0DUB zr{s;Zv{{cLUS1n94VnS(k@q8EC+VAwd(mElzOz)Ku(vdn?5~e}mSYr67f>0c6L}9^ z^78MzSUPo5Uc+xnrDdF;K6AT!IC<_*11-DjpmKKo))d#Br+=FMP$LWP_($?Bl#Gtm zU(T89y~XnDVgU2*Umdh~FS(dK6SthVanI6?(YT)FdUl-t-7HjtyQt{;8w2`LwRo|K zE)B|9;B%+bTg8uMJP;+*6G&8@q}`)~kg?$Tvtsb4{Z9mISvIY0t|d*bh$Zv1jiFE{ z`^7lXk~C>E_l!!F?fjGO2cK_u`#u!lmVEWueseFY=k63~Z8RpU!*k#2&-f6u;H|CJhf^7D- zcBW3*GUnR_Rz++&rCS$N9HVN|Qin%{2C41hxV!fj<@-ukR6-&O)78pKHDTJBFd5YK z)*uf8WO-qsGO%K{Yuq+k6==cV9{cYg!zNCeYbb92hwJmH&eEDR|U6c zsJfA#ixbiwreE3K5o$m?Iury{$e=Vc=I+;saIzV%|Cj_Vcl< zKifa(2*OTRa8&OBC$sl}YlF(!&G<+KC~`J3m#Ki?oNy&L2R|o>gXiC$Z}z1Cgu>x%=XGU!0U*F%FO)6(*9%~K z#kl1eyJi3dQNVxV{;E)*1DFE@V7#;fXmDCGSXKa8fC0DpBWu7>DI6Gpg3D=wdBsI| zxWF86IS@cXlb@R#!9ZFA;yBrRYz@H5{*45JfPW)3KwSTe1hONKaVs+g&ukT;a}4yCx`$5 diff --git a/aptos-move/framework/move-stdlib/sources/string.spec.move b/aptos-move/framework/move-stdlib/sources/string.spec.move index 140b8e728fc..78f688043bf 100644 --- a/aptos-move/framework/move-stdlib/sources/string.spec.move +++ b/aptos-move/framework/move-stdlib/sources/string.spec.move @@ -24,6 +24,12 @@ spec std::string { String{bytes} } + spec utf8(bytes: vector): String { + pragma opaque; + aborts_if !spec_internal_check_utf8(bytes); + ensures result == spec_utf8(bytes); + } + spec module { fun spec_internal_check_utf8(v: vector): bool; fun spec_internal_is_char_boundary(v: vector, i: u64): bool; diff --git a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl index 5cbf7569f91..693799fe5ef 100644 --- a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl +++ b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl @@ -226,6 +226,43 @@ procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), i: int, } } +// `vector::move_range(from, removal_position, length, to, insert_position)` extracts the +// half-open range `[removal_position, removal_position+length)` from `from` and splices it +// into `to` at `insert_position`, shifting `to[insert_position..]` to the right. Move enforces +// that `from` and `to` are distinct (no aliasing of mutable references). +procedure {:inline 1} $1_vector_move_range{{S}}( + from: $Mutation (Vec ({{T}})), + removal_position: int, + length: int, + to: $Mutation (Vec ({{T}})), + insert_position: int +) returns (from': $Mutation (Vec ({{T}})), to': $Mutation (Vec ({{T}}))) +{ + var from_v: Vec ({{T}}); + var to_v: Vec ({{T}}); + var middle: Vec ({{T}}); + from_v := $Dereference(from); + to_v := $Dereference(to); + // The `< 0` checks are defensive — Move's u64 arguments are non-negative by typing, + // but Boogie ints can be arbitrary so we guard explicitly. Matches the convention + // used in `$1_vector_insert` above. + if (removal_position < 0 + || length < 0 + || removal_position + length > LenVec(from_v) + || insert_position < 0 + || insert_position > LenVec(to_v)) { + call $ExecFailureAbort(); + return; + } + middle := SliceVec(from_v, removal_position, removal_position + length); + from' := $UpdateMutation(from, + ConcatVec(SliceVec(from_v, 0, removal_position), + SliceVec(from_v, removal_position + length, LenVec(from_v)))); + to' := $UpdateMutation(to, + ConcatVec(SliceVec(to_v, 0, insert_position), + ConcatVec(middle, SliceVec(to_v, insert_position, LenVec(to_v))))); +} + procedure {:inline 1} $1_vector_length{{S}}(v: Vec ({{T}})) returns (l: int) { l := LenVec(v); }