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

Commits on master

Daniel Schoepe
Run smoke CI tests on Linux (#3375)
committed
Daniel Schoepe
Get `isize` width from rustc rather than platform where verus is built (#3373)
committed
Travis Hance
forbid unsafe attrs (#3362)
committed
Chris Hawblitzel (Microsoft)
Support opens_invariants in proof closures (#3199)
committed
Bryan Parno
Swap from will_return_none to produces (#3330)
committed
Bryan Parno
Make NonZero specifications available in default Cargo builds. (#3361)
committed
Matthew Dwyer
verification observer: interface to capture information about VC lowering (#2965)
committed
Martin Mirchev
Report pending HIR→VIR diagnostics on every exit path (#3317)
committed
Michael Tautschnig
verus!: fields named like Verus keywords (#3230)
committed
Nick Giannarakis
Restore the visitor mode after nested items in verus! (fixes #3134) (#3222)
committed
wsxarcher.tngl.sh
vstd: Add <[T]>::swap (#3357)
committed
Travis Hance
Guide typos (#3340)
committed
Yi Wu
vstd: make slice_to_vec copy its elements instead of calling to_vec (#3343)
committed
Michael Tautschnig
Confirm assertion labels before reporting errors when several are true in the model (#3240)
committed
Michael Tautschnig
prune: keep invariant-mask set operations when a mask cannot be determined (#3245)
committed
zhengyao
exec_spec macro: replace ExecSpecEq with PartialEq + ObeysDeepEq (#3351)
committed
Máté Kovács
[CI] feat: optimize release archive size (#3350)
committed
Daniel Schoepe
Use hygienic names for Verus-generated identifiers in for loops (#3355)
committed
Chris Hawblitzel (Microsoft)
In verita, restore vest (#3353)
committed
Travis Hance
Integrate Query into rustc query system (#3316)
committed
Máté Kovács
[ci] fix: add MacOS allow gatekeeper script to release archives (#3348)
committed
Máté Kovács
[makefile] fix: make `build-vstd` depend on `install` (#3346)
committed
Bryan Parno
Add toolchain manifest for Release 0.2026.10.26.d17fbd0 (#3341)
committed
Chris Hawblitzel (Microsoft)
Rename `#[verifier::verify]` to internal name (#3324)
committed
Travis Hance
Diagnostic messages copy-editing (#3335)
committed
Snehal Reddy
doc(guide): Fix variable typo in lemma_mod_between comments (#3336)
committed
Bryan Parno
Update crate version numbers (#3333)
committed
Chris Hawblitzel (Microsoft)
verita patch (#3332)
committed
Xiangdong Chen
Fix unsound opaque type assumptions at function returns (#3112)
committed
Bryan Parno
Tidy up the iterator interface (#3326)
committed
Martin Mirchev
Hint when a failing termination check is inside a spec closure (#3315)
committed
Bryan Parno
Fix external-trait associated bounds (#3295)
committed
Travis Hance
rust_verify_test: record each test's sources and logs (#3323)
committed
Nick Giannarakis
use FnDef(method, trait_typ_args + method_typ_args) instead of FnDef... (#3306)
committed
wsxarcher.tngl.sh
vstd: add cmp::min* cmp::max* free functions (#3276)
committed
Chris Hawblitzel (Microsoft)
Check that exec code doesn't match on ghost enums/consts/ranges/slices (#3321)
committed
Travis Hance
flip order of crate vs other crates in merge_traits (#3320)
committed
Travis Hance
Big verification.rs pipeline refactor (#3236)
committed
Nick Giannarakis
require RangeBounds impls to satisfy their spec bounds (#3314)
committed
Martin Mirchev
vstd: specify core::panicking::assert_failed so assert_eq! can be used (#3273)
committed
Langston Barrett
doc(guide): Add an example of the `matches` operator (#3084)
committed
Kasim Te
vstd: add specs for slice get_unchecked(_mut) and split_at_unchecked(_mut) (#3272)
committed
Martin Mirchev
vstd: specify <Vec as AsRef<[T]>>::as_ref, like as_slice (#3274)
committed
Martin Mirchev
vstd: add u128 and i128 to the NonZero is_zero spec (#3275)
committed
Martin Mirchev
Publish Linux and Windows arm64 release builds (#3292)
committed
Nick Giannarakis
check bounds for exec_update (#3312)
committed
Daniel Schoepe
Mode-check anonymous Rust constants through VIR (fix #3155) (#3305)
committed
Bryan Parno
Fix activate script and vargo's cvc5 version matching (#3308)
committed
Travis Hance
add copyable resource for RA and SP interfaces (#3303)
committed
Máté Kovács
[rust_verify] fix: add Verus version to `rust_verify -vV` output (#3289)
committed
Nick Giannarakis
Add fmt_req to requires for to_string and formatting arguments (#3150)
committed
Travis Hance
forbid break/continue in proof blocks (#3286)
committed
Nick Giannarakis
Parameterize IEEE float ops by float type (#3285)
committed
Travis Hance
fix --help message for --export (#3297)
committed
Lacramioara Astefanoaei
vstd: add u128 instances of the shift and mask lemmas in bits.rs (#3129)
committed
Máté Kovács
[cargo-verus] feat: add Verus version to Cargo metadata hash (#3281)
committed
Martin Mirchev
Bind inherited trait-method specs to the impl method's own type params (#3118)
committed
Bryan Parno
Include will_return_none as part of the definition of from_iter_ensures (#3264)
committed
Bryan Parno
Improve our specifications for from_iter (#3259)
committed
Daniel Schoepe
Emit absolute paths to core/vstd items (#3279)
committed