verus
forked from verus-lang/verus
Star 0
Fork 0
Watch

Version history of source/vstd/std_specs/vec.rs

October 2026

Bryan Parno
Swap from will_return_none to produces (#3330)
committed
Martin Mirchev
vstd: specify <Vec as AsRef<[T]>>::as_ref, like as_slice (#3274)
committed
Bryan Parno
Include will_return_none as part of the definition of from_iter_ensures (#3264)
committed
Anton Yarkov
Specify Vec::try_reserve_exact in vstd (#3094)
committed
AJ Weeks
vstd: add no_unwind to vec, array, slice (#3226)
committed

September 2026

Chris Hawblitzel (Microsoft)
Use Seq range syntax in vstd, examples, docs (#2959)
committed
Travis Hance
add some tracked borrow fns for PointsTo, Vec, and slice (#2884)
committed
Chris Hawblitzel (Microsoft)
Add get and get_mut specs for SliceIndex, refactor slice::get spec (#2895)
committed

August 2026

Bryan Parno
Remove initial_value_relation and infer_spec_for_loop_iter (#2739)
committed

July 2026

Bryan Parno
Use the loop_isolation_boundary feature to simplify our specs for Rust iterators. (#2736)
committed
Chris Hawblitzel (Microsoft)
Index mut (merge) (#2727)
committed
Baltasar Dinis
vstd: remove usage of group_seq_axioms and added axioms (#2678)
committed

May 2026

Bryan Parno
Add basic support for Iter::collect (#2449)
committed
Chris Hawblitzel (Microsoft)
Add trait bound to spec == operator to improve type inference (#2377)
committed
Bryan Parno
New approach to specifying iterators via a prophetic sequence encoding (#2163)
committed
Travis Hance
support DerefMut (#2411)
committed
Travis Hance
update vstd to use the new_mut_ref style (#2408)
committed

April 2026

Jay Lorch
Merge remote-tracking branch 'upstream/main' into fix-2290
committed
Chris Hawblitzel (Microsoft)
Rename laws_eq::obeys_eq_spec and laws_cmp::obeys_cmp_spec (#2327)
committed
Chris Hawblitzel (Microsoft)
Translate general case of ExprKind::Index into calls to Index::index (#2300)
committed

March 2026

Travis Hance
add decreases axiom for Vec (#2255)
committed
Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed

February 2026

Travis Hance
implement 'final' operator (#2193)
committed
Travis Hance
new-mut-ref: handle old function properly (#2190)
committed
Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed

January 2026

项科深 Xiang Keshen
add default trait, some option specs and string deref (#2064)
committed

December 2025

Travis Hance
vstd: add some more slice specs
committed
Travis Hance
new-mut-ref: add 'fin' builtin (name not finalized)
committed
Travis Hance
new-mut-ref: specs for Vec
committed
Jay Lorch
Specification for Vec::try_reserve (#2045)
committed
Chris Hawblitzel
Merge branch 'main' into seq-lemmas-triggers
committed
Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed

November 2025

Hiroki Chen
Fix generics for `Vec` with allocator APIs (#2004)
committed
Travis Hance
support vec_from_elem; fixes #1952 (#1983)
committed
Daniel Schoepe
Add specification for Vec::is_empty (#1940)
committed

October 2025

Chris Hawblitzel
Merge branch 'main' into nonblocking_external_error
committed

September 2025

Chris Hawblitzel
Declare PartialEq for Vec
committed

July 2025

Bryan Parno
Prepare Verus-related crates for posting to crates.io (#1815)
committed
Chris Hawblitzel
Simplify Vec::swap_remove
committed
lyj
Vec::swap_remove (#1755)
committed

June 2025

Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Chris Hawblitzel
Merge branch 'main' into loop-infer-base
committed
Chris Hawblitzel
Update when_used_as_spec to account for traits
committed
Chris Hawblitzel
Minor edits to vec/vecdeque iterator specs
committed
Baltasar Dinis
std_specs: add support for Vec iteration via Vec::into_iter (#1686)
committed

May 2025

Chris Hawblitzel (Microsoft)
Support deref coercion adjustments (#1710)
committed
Travis Hance
add no_unwind to vec index and vec len (#1613)
committed
Travis Hance
implement autospec feature for 'returns' clause (#1643)
committed

March 2025

Andrea Lattuada
uninterp marker on uniterpreted spec fns (#1473)
committed
ziqiaozhou
A solution to avoid using .set() function by replacing IndexMut with index_set (#1476)
committed