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

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

October 2026

Bryan Parno
Swap from will_return_none to produces (#3330)
committed
Nick Giannarakis
require RangeBounds impls to satisfy their spec bounds (#3314)
committed
Bryan Parno
Minimal fix for restricting the use of IteratorSpecImpl spec functions. (#3277)
committed
Bryan Parno
Match our specs for the length and bounds of RangeInclusive to those used in std (#3249)
committed

August 2026

Chris Hawblitzel (Microsoft)
Fix RangeInclusive::end_bound, switch from SpecBound to Bound (#2801)
committed
Martin Mirchev
vstd: fix unsound RangeInclusive::end_bound spec for exhausted ranges (#2687)
committed
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

June 2026

Ruize Tang
vstd: add `RangeBounds` and slice `copy_within`/`copy_from_slice` specs (#2569)
committed
Ziqiao Zhou
vstd/range: implement IteratorSpecImpl for RangeInclusive (#2479)
committed

May 2026

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

November 2025

ziqiaozhou
Add RangeInclusive::contains and new (#1966)
committed

July 2025

Chris Hawblitzel
Add is_lt, is_le, etc. blanket impl wrappers around eq_spec, partial_cmp_spec
committed
ziqiaozhou
Add spec for range contains (#1806)
committed

March 2025

Andrea Lattuada
uninterp marker on uniterpreted spec fns (#1473)
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

July 2024

Jay Bosamiya (Microsoft)
Minor one-line change due to verusfmt 0.4.0 (#1233)
committed

May 2024

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

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
verusfmt
committed
Andrea Lattuada
apply generalized broadcast to vstd
committed

March 2024

Andrea Lattuada (VMware)
Generalized lemma broadcast, implements #37 (#1022)
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