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

Version history of source/vstd/array.rs

October 2026

AJ Weeks
vstd: add no_unwind to vec, array, slice (#3226)
committed

September 2026

Jay Lorch
Decreases for arrays and slices (#2888)
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

May 2026

Chris Hawblitzel (Microsoft)
Add trait bound to spec == operator to improve type inference (#2377)
committed
Travis Hance
deprecate the set function for arrays/slices (#2423)
committed
Bryan Parno
New approach to specifying iterators via a prophetic sequence encoding (#2163)
committed
Travis Hance
update vstd to use the new_mut_ref style (#2408)
committed

March 2026

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

Travis Hance
new-mut-ref: support the unsizing coercion `&mut [T; N] -> &mut [T]`
committed

December 2025

Travis Hance
broadcast axiom_array_has_resolved and axiom_slice_has_resolved (#2046)
committed
Travis Hance
new-mut-ref: fix some encoding issues and add has_resolved axiom for arrays and slices
committed
Travis Hance
new-mut-ref: add slice/array indexing to Place (#2035)
committed

June 2025

Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Chris Hawblitzel
Merge branch 'main' into add-decreases
committed
Travis Hance
array and slice extensionality, fixes #1670 (#1765)
committed

May 2025

Travis Hance
Add an 'axiom' keyword (#1518)
committed

March 2025

Andrea Lattuada
uninterp marker on uniterpreted spec fns (#1473)
committed

February 2025

Travis Hance
Update VIR representation of open/closed/opaque (#1452)
committed
Alex Bai
Seq_lib broadcasting (#1436)
committed

January 2025

Travis Hance
add better syntax for external_fn_specification (#1368)
committed

August 2024

Chris Hawblitzel (Microsoft)
Prune broadcast functions based on their triggers (#1175)
committed
Chris Hawblitzel
Update the encoding of array literals to auto-trigger each element (e.g. for array literal a = [10, 20, 30] auto-trigger a@[0], a@[1], a@[2])
committed

July 2024

Bryan Parno
Add support for array literals (#1198)
committed

May 2024

Travis Hance
Support array-repeat expressions [x; N]
committed
Travis Hance
Support embedding 'builtin' and 'vstd' as modules in order to support verifying core (#1085)
committed
Chris Hawblitzel
Update verifier(...) to verifier::... in guide/examples/vstd
committed
Chris Hawblitzel (Microsoft)
Implement View and DeepView in slice and array (#1078)
committed

April 2024

Andrea Lattuada
Use generalized broadcast in arithmetic library, rename all broadcast groups to have the prefix group_ (#1086)
committed
Andrea Lattuada
Merge pull request #1023 from verus-lang/generalized-broadcast-vstd
committed
Andrea Lattuada
support cfg(not(feature = "alloc")) with default vstd broadcast group, guard verifier attributes with cfg_attr where necessary
committed
Andrea Lattuada
fix failing proofs, use new broadcast mechanism for array_as_slice
committed
Andrea Lattuada
apply generalized broadcast to vstd
committed
Travis Hance
add vec/array/slice functions to verus_items
committed

March 2024

Travis Hance
fix deprecation warning in vstd
committed
Andrea Lattuada (VMware)
Generalized lemma broadcast, implements #37 (#1022)
committed
Jay Bosamiya
Add `verusfmt --check` to CI (#1019)
committed
verusfmt
Reformat latest vstd on latest `main`
committed
Travis Hance
support array to slice conversions
committed

February 2024

Bryan Parno
Merge pull request #1004 from verus-lang/apply-verusfmt
committed
verusfmt
Format vstd with `verusfmt` version 0.2.3
committed
Andrea Lattuada
rename pervasive -> vstd
committed