Skip to content

QCP-v2.1.0

Latest
Latest

Choose a tag to compare

View all tags
@yashen32768 yashen32768 released this 13 Aug 07:25
· 1 commit to main since this release
QCP-v2.1.0
8ed089e

QCP v2.1.0 Release Notes

We are pleased to announce QCP v2.1.0. This release is centered on two major milestones: Lean proof-backend support and a substantial update to the verified CDCL SAT solver example.

What's New

Lean Proof-Backend Support

QCP now supports Lean as a proof backend alongside Rocq. The latest binaries can generate Lean verification conditions and strategy outputs, allowing users to choose the backend that best fits their project.

This release includes:

  • a Lean library tree covering the foundations required by QCP, including sets, auxiliary libraries, CompCert-style integers, monadic libraries, separation logic, and related infrastructure;
  • generated Lean files and checked proofs for a representative collection of QCP examples;
  • Linux and Windows scripts for generating Lean artifacts from the QCP_demos_LLM examples;
  • documented build and editor workflows for Linux, macOS, and native Windows; and
  • a backend-specific repository layout, with Rocq libraries under Rocq/ and Lean libraries under Lean/.

Lean and Rocq are independent proof-backend choices. Users only need to install the backend they intend to use; both are required only when generating and checking both .lean and .v artifacts.

Updated and Verified CDCL Example

We spent a focused week completing the verification of the CDCL SAT solver example. The updated example now connects the annotated C implementation, abstract CDCL state, strategy rules, generated verification conditions, and modular Rocq proofs in one checked workflow.

The verification covers the solver's key state transitions, including initialization, Boolean constraint propagation, decisions, conflict handling, clause learning, and backjumping. Its checked contract establishes that the solver returns:

  • 1 only with an assignment that satisfies the original formula;
  • 0 only with an unsatisfiability certificate; and
  • -2 when the configured conflict budget is exhausted, without making a claim about satisfiability.

The result is a larger, more realistic end-to-end QCP example. The proof establishes partial functional correctness; termination is outside the current contract.

Improvements

Verification Features

  • Added architecture- and endianness-aware proof generation for 32-bit and 64-bit targets and for big- and little-endian memory models.
  • Parameterized pointer size, pointer-store layout, and address-space bounds by the selected architecture.
  • Improved symbolic execution for complex array and struct initialization and for memory layouts combining arrays, structs, and field access.
  • Added generated builtin predicates and strategies for supported struct types, with the corresponding definitions emitted in generated def.v files.

QIDE

  • Improved highlighting load time when opening annotated C sources and generated verification artifacts.
  • Updated the bundled QIDE extension to match the latest QCP binary and generated-file formats.

Repository Examples and Proof Maintenance

  • Regenerated repository examples against the latest binary and ported affected manual proofs to the new goal shapes.
  • Refactored large and repetitive example proofs into more maintainable shared libraries and proof modules.
  • Refreshed strategy outputs, generated checks, demo indexes, and example statistics.
  • Clarified ownership between generated proofs and manual proofs to reduce duplicate proof fields and unnecessary proof churn after regeneration.

For reusable migration patterns, see the QCP v2.1.0 proof-porting guide.

Migration Notes

  • Choose either the Lean or Rocq workflow for normal use. Follow Lean/README.md when building and checking the Lean backend.
  • Proofs that assumed sizeof(PTR) = 4 should be checked against the current architecture setting. Use architecture-parametric lemmas for portable proofs and explicit 32-bit compatibility lemmas only where the proof is intentionally 32-bit-specific.
  • Update scripts and imports that still refer to the former top-level SeparationLogic path; Rocq-specific paths now use Rocq.
  • Regenerate verification conditions before repairing manual proofs, and do not patch generated goal, auto, or goal_check files by hand.
  • Reinstall or reload the bundled QIDE extension from qide.vsix to pick up the latest highlighting and compatibility updates.

Happy verifying with QCP v2.1.0!

Assets 2
Loading