Skip to content

NonZero (unchecked_mul & unchecked_add) Proof for Contracts #338

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 45 commits into from
Jun 14, 2025
Merged
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
dffe30b
Initial proof/contract/harness for nonzero:
aa-luna Sep 20, 2024
daf1576
Bytewise comparision (new_unchecked contract)
SahithiMV Oct 6, 2024
21ae29e
Removed kani assumes removed from proof_for_contract
aa-luna Oct 8, 2024
4241687
Macros for data types
SahithiMV Oct 13, 2024
801f9a4
Adding i32 and isize
SahithiMV Oct 13, 2024
eafef0b
Pull Request fixes
aa-luna Oct 20, 2024
3015feb
Pull Request fixes
aa-luna Oct 21, 2024
ce918f8
Update library/core/src/num/nonzero.rs
MooniniteErr Oct 27, 2024
2304fad
Update library/core/src/num/nonzero.rs
MooniniteErr Oct 27, 2024
14a50e2
Update library/core/src/num/nonzero.rs
aa-luna Oct 27, 2024
acef65a
Update library/core/src/num/nonzero.rs
aa-luna Oct 27, 2024
4d3efd1
Update library/core/src/num/nonzero.rs
aa-luna Oct 27, 2024
7bc64eb
doc: add explanations for const function attribute
aa-luna Nov 3, 2024
82ff59c
Merge branch 'main' into main
aa-luna Nov 8, 2024
4ce34b5
Merge branch 'main' into main
aa-luna Nov 9, 2024
f81aa80
Merge branch 'model-checking:main' into main
aa-luna Nov 12, 2024
b2b534b
Merge branch 'model-checking:main' into main
aa-luna Nov 16, 2024
dcbf4f5
Merge branch 'model-checking:main' into unchecked_mull_add
aa-luna Nov 24, 2024
d67be7e
Unchecked Add and Mul: Init
SahithiMV Nov 24, 2024
36e75be
Unchecked Mul and Add: Adding Macros & cleanup
SahithiMV Nov 26, 2024
4f945c8
Fixes
SahithiMV Dec 9, 2024
fb30e98
Merge remote-tracking branch 'origin/main' into unchecked_mull_add
tautschnig Apr 23, 2025
71e57fa
Apply suggestions
tautschnig Apr 23, 2025
fcfd000
Arrange lines
tautschnig Apr 23, 2025
7603984
Add contract to from_mut_unchecked
tautschnig Apr 23, 2025
6dab042
Fix syntax error, naming
tautschnig Apr 23, 2025
06fad10
Disable what does not currently compile
tautschnig Apr 23, 2025
d8e3977
Proof target names
tautschnig Apr 23, 2025
014a44e
Contracts lookup, again
tautschnig Apr 23, 2025
0a7a3c6
Lookup, once more
tautschnig Apr 24, 2025
fb8ad3e
rustfmt
tautschnig Apr 24, 2025
0c0318f
Merge remote-tracking branch 'origin/main' into unchecked_mull_add
tautschnig Apr 24, 2025
3b69e21
rustfmt 2
tautschnig Apr 24, 2025
8bd1151
Remove stray space
tautschnig Apr 24, 2025
233c41c
Update library/core/src/num/nonzero.rs
tautschnig Apr 28, 2025
d21fdf2
Update library/core/src/num/nonzero.rs
tautschnig Apr 28, 2025
5f13ef4
Update library/core/src/num/nonzero.rs
tautschnig Apr 28, 2025
36030a8
Update library/core/src/num/nonzero.rs
tautschnig Apr 28, 2025
1c5b394
Update library/core/src/num/nonzero.rs
tautschnig Apr 28, 2025
f2667db
Merge remote-tracking branch 'origin/main' into unchecked_mull_add
tautschnig Apr 29, 2025
ebfd876
Remove from_mut_unchecked contract/harnesses (commented out)
tautschnig Apr 29, 2025
cc23429
Merge remote-tracking branch 'tautschnig/unchecked_mull_add' into unc…
tautschnig Apr 29, 2025
2e6ccae
Adjust target lookup
tautschnig Apr 30, 2025
cd7db54
Merge branch 'main' into unchecked_mull_add
tautschnig May 20, 2025
f67539e
Add comment
tautschnig May 30, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update library/core/src/num/nonzero.rs
Co-authored-by: Zyad Hassan <[email protected]>
  • Loading branch information
aa-luna and zhassan-aws authored Oct 27, 2024
commit 4d3efd16f6e03a3dbeeba497ebf6b6c843dc5168
2 changes: 1 addition & 1 deletion library/core/src/num/nonzero.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2193,7 +2193,7 @@ nonzero_integer! {

#[unstable(feature="kani", issue="none")]
#[cfg(kani)]
mod verify {
mod verify {
use super::*;

macro_rules! nonzero_check {
Expand Down
Loading