Challenge 12: Verify safety of NonZero - #565

Closed

Samuelsills wants to merge 7 commits into

model-checking:mainfrom

Samuelsills:challenge-12-nonzero

Commits on Mar 24, 2026

Challenge 12: Verify safety of NonZero
Samuelsills
committed
71e54d0

Commits on Apr 1, 2026

Address reviewer feedback: add semantic correctness assertions

Samuelsills
and
claude
committed
6cdcb52
Bound checked_pow/saturating_pow exponent to avoid CI timeout

Samuelsills
and
claude
committed
c99f265
Reduce pow harnesses to small types for CI autoharness tractability

Samuelsills
and
claude
committed
cb26d8e

Commits on Apr 2, 2026

Merge upstream main (Copilot review config + Kani metrics)
Samuelsills
committed
e7fd1d4
Fix CI: restore pow harnesses to full type coverage without unwind

Samuelsills
and
claude
committed
f1db6c0

Commits on Apr 3, 2026

Fix CI: revert to original harnesses + add targeted correctness proofs

Samuelsills
and
claude
committed
dd226f4