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

Version history of source/vstd/bits.rs

October 2026

Lacramioara Astefanoaei
vstd: add u128 instances of the shift and mask lemmas in bits.rs (#3129)
committed

July 2026

Bryan Parno
Upgrade to Z3 4.16.0 (#2578)
committed

April 2026

Jay Lorch
Merge remote-tracking branch 'upstream/main' into fix-2290
committed
Jay Lorch
Merge pull request #2310 from mmcloughlin/vstd-bits-opt-lemma_uN_shr_is_div
committed
Michael McLoughlin
move comment
committed
Michael McLoughlin
vstd: step by 4
committed

March 2026

Chris Hawblitzel
Merge branch 'main' into ieee-float
committed
Luo Jia / Zhouqi Jiang
Add bit lemmas for `usize` type (#2225)
committed
Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed

February 2026

Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed
elanortang
Add layout axioms (#2119)
committed

July 2025

Theodore Ehrenborg
Add lemma_u128_shr_is_div (#1844)
committed

June 2025

Xinyi Wan
Add bits lemmas (#1787)
committed
Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Chris Hawblitzel
Merge branch 'main' into loop-infer-base
committed
Alex Bai
make arithmetic::pow opaque (#1714)
committed

May 2024

Travis Hance
Support embedding 'builtin' and 'vstd' as modules in order to support verifying core (#1085)
committed
Michael McLoughlin
vstd: broadcast bits lemmas (#1119)
committed
verusfmt
Update formatting for `calc!` statements
committed
Bryan Parno
Add a missing semi-colon
committed
Michael McLoughlin
vstd: bitwise mask properties (#1063)
committed

April 2024

Bryan Parno
Merge pull request #1054 from mmcloughlin/shr-is-div
committed
Michael McLoughlin
vargo fmt
committed
Michael McLoughlin
verus_keep_ghost
committed
Michael McLoughlin
use <$uN>:: syntax
committed
Michael McLoughlin
lemma_uN_pow2_no_overflow_auto
committed
Michael McLoughlin
lemma_uN_shl_is_mul_auto
committed
Michael McLoughlin
doc for lemma_shl_is_mul
committed
Michael McLoughlin
lemma_shl_is_mul
committed
Michael McLoughlin
use u64::MAX
committed
Michael McLoughlin
vargo fmt
committed
Michael McLoughlin
lemma_u64_shl_is_mul
committed
Michael McLoughlin
move asserts into calc macro
committed
Michael McLoughlin
include type name in doc string
committed
Michael McLoughlin
lemma macro for all unsigned types
committed
Michael McLoughlin
vargo fmt
committed
Michael McLoughlin
lemma_u64_shr_is_div_auto
committed
Michael McLoughlin
lemma_u64_shr_is_div
committed