Verify safety of NonZero operations (Challenge 12) - #544

Open

jrey8343 wants to merge 7 commits into

model-checking:mainfrom

jrey8343:challenge-12-nonzero

Commits on Feb 8, 2026

Verify safety of NonZero operations (Challenge 12)
jrey8343
committed
a698020

Commits on Feb 11, 2026

Apply upstream rustfmt formatting via check_rustc.sh --bless
jrey8343
committed
8267fcb

Commits on Feb 21, 2026

Use bounded exponent for NonZeroI128/U128 saturating_pow harnesses
jrey8343
committed
b23d05f
Fix checked_pow_i128/u128 CBMC timeout: bound exponent to avoid explosion
jrey8343
committed
9d26114

Commits on Apr 2, 2026

Add missing isqrt harnesses for u64, u128, and usize
jrey8343
committed
b16b2db

Commits on Aug 18, 2026

Restore checked_pow loop invariants; scope workaround to pow harnesses

jrey8343
and
claude
committed
a432b6e
Fix isqrt harness CI timeouts with bounded intervals for wide types

jrey8343
and
claude
committed
049188b