QCP v2.1.4 expands Lean verification coverage, adds floating-point conversion support in Rocq, and improves proof generation and build compatibility across platforms.
What's New
Expanded Lean Verification Support
- Expanded Lean coverage for algorithm, data-structure, and Codeforces benchmarks, including case libraries, generated verification conditions, and manual proofs.
- Completed all 281 proof obligations across 26 supported demo strategy sets.
- Replaced placeholder shape predicates with definitions aligned with the Rocq backend.
- Extended supporting array, list, and monadic reasoning libraries.
- Consolidated reusable proof helpers and removed obsolete migration artifacts.
Floating-Point Format Conversions
Added Rocq definitions and supporting lemmas for conversions between 32-bit, 64-bit, and 128-bit floating-point formats.
- Added widening and narrowing conversions used by generated verification conditions for C casts.
- Proved exactness of widening conversions on finite inputs.
- Added rounding lemmas for narrowing conversions when the result does not overflow.
- Handled signed zeros, infinities, and NaNs consistently with the existing floating-point library.
More Codeforces Examples
Expanded the Codeforces example collection with annotated C programs, supporting Rocq libraries, verification conditions, and proofs. Updated generation runners and build configurations to include the additional examples.
Improvements
Native Proof Generation
- Added manifest-based Lean generation scripts for Windows and Unix environments, covering both program and strategy inputs.
- Preserved existing reviewed Lean proofs when refreshing generated goals and goal checks.
- Expanded Rocq generation coverage and refreshed stale generated artifacts.
- Updated the bundled QCP binaries for Windows, Linux, macOS arm64, and macOS x86-64.
Proof and Build Maintenance
- Adapted Rocq and Lean proofs to refreshed verification conditions and annotation interfaces.
- Split expensive proofs into smaller components.
- Updated Dune, Make, and Lake build configurations for the expanded example suite.
- Made the shared Coq checking timeout configurable for longer-running proofs.
Bug Fixes
- Fixed missing Rocq definitions for floating-point conversions emitted by symbolic execution.
- Fixed Windows command-line length failures by splitting large Dune theories while preserving logical import paths.
- Shortened Windows generation staging paths to avoid path-length issues.
- Fixed qualified Rocq imports in graph examples.
- Removed manual proof declarations duplicated by generated automatic proofs.
- Repaired Lean annotation and generated-goal compatibility issues.
Happy verifying with QCP v2.1.4!