Skip to content

QCP-v2.0.4b

Choose a tag to compare

View all tags
@yashen32768 yashen32768 released this 20 Jul 02:11
· 2 commits to main since this release
QCP-v2.0.4b
51d9ff9

QCP v2.0.4b Release Notes

QCP v2.0.4b is a maintenance release for the v2.0.4 line. It focuses on bug fixes, a broader example set, improvements to the LLM-assisted proof workflow, and a refreshed QIDE extension.

What's New

Expanded Example Coverage

This release adds and refreshes more verification examples across the repository, with particular attention to floating-point programs.

  • Added more generated goals, proof files, and example runners for the current example suite.
  • Expanded floating-point coverage, including tutorial-level float examples and larger algorithmic float cases.
  • Added floating-point-oriented benchmark material such as LLM_bench/Algorithms/convex_hull_float.
  • Refreshed example metadata used by the example lists, strategy summaries, and benchmark helpers.

These examples are intended both as user-facing references and as regression coverage for symbolic execution, generated VCs, and Rocq proof checking.

QIDE Extension Updates

The bundled QIDE VS Code extension has been updated.

  • Added highlighting support for C code used in QCP verification workflows.
  • Refined the display of the current verification state.
  • Updated lspPath handling so it now matches the documented behavior: users can set it to an explicit path, while still being able to point it directly at the appropriate lsp binary.
  • Updated the packaged qide.vsix in the repository root.

The extension should now give clearer feedback while users inspect annotated C programs and follow the current symbolic-execution or proof status.

Bug Fixes and Workflow Improvements

LLM-Assisted Proof Workflow

The LLM proof workflow no longer copies the entire repository when preparing an isolated worktree for proof tasks. Instead, the workflow now keeps proof preparation scoped to the files and run directories that are needed for the current verification task.

This avoids unnecessary disk usage, reduces setup time for proof attempts, and makes intermediate verification runs easier to inspect.

General Fixes

This release also includes a collection of smaller fixes across the toolchain and generated artifacts.

  • Fixed bugs found while regenerating and checking the expanded example set.
  • Refreshed generated Rocq files for affected examples.
  • Updated platform binaries and helper scripts to match the current symbolic-execution and proof workflow.
  • Improved consistency between example source files, generated goals, auto proofs, manual proofs, and goal checks.

Migration Notes

  • Users of v2.0.4 can treat v2.0.4b as a compatible maintenance update.
  • Regenerated VCs may still differ for examples touched by bug fixes or floating-point support improvements; proof scripts should be checked against the current generated goals.
  • If you use the LLM-assisted proof workflow, old runs that assumed full-repository copied worktrees should be refreshed with the current controller workflow.
  • Reinstall or reload the bundled QIDE extension from qide.vsix to pick up the C-code highlighting, current-status display changes, and updated lspPath behavior.

Happy verifying with QCP v2.0.4b!

Assets 2
Loading