QCP-v2.0.3

QCP v2.0.3 Release Notes

We are excited to announce the release of QCP v2.0.3! This update focuses on improving AI-assisted proof migration, expanding the verified example suite, refreshing the cross-platform verification toolchain, and adding new libraries for symbolic execution and formal reasoning.

What's New

🤖 AI-Assisted Version Migration with Version_Log

• Added Version_Log/ to help users migrate proofs across QCP versions with the support of AI assistants.
• The version logs summarize proof-breaking generator changes, common VC drift patterns, branch and witness-numbering changes, and practical repair strategies.
• These notes are intended to make AI-assisted proof repair more reliable by giving both users and assistants a structured migration guide instead of relying only on raw generated goals.

🔧 Refreshed Cross-Platform QCP Toolchain

• Updated the QCP binary tools for Windows, Linux, macOS arm64, and macOS x86-64.
• Refreshed symexec, mcp, lsp, and StrategyCheck across supported platforms.
• Updated example execution scripts so symbolic execution commands better match the current include-path and logic-path requirements.
• Updated rocq-mcp and the agent-oriented proof workflow documentation to align with the current Rocq proof loop.

🧵 Shared StdLib String Support

• Added shared string extraction support through QCP_examples/stdlib/string.h and QCP_examples/stdlib/string.strategies.
• Moved reusable string predicates, result specifications, helper lemmas, and strategy proofs into SeparationLogic/stdlib/string_lib.v.
• Kept compatibility wrappers for older Engineering string imports, making the transition smoother for existing examples.

∑ SumLib and minigmp_sumlib

• Integrated SeparationLogic/SumLib, a finite-sum and range-oriented support library for arithmetic and list proofs.
• Added and refreshed the minigmp_sumlib verification example.
• Documented migration guidance for list_to_Z, Sum.sum, regenerated VCs, and proof drift caused by branch or witness-numbering changes.

🔁 Safeexec Refinement Workflow Updates

• Simplified the safeexec refinement flow by removing older equiv and direct program_equiv obligations.
• High-level specifications are now derived through Hoare_safeexec_compose.
• Regenerated and repaired affected safeexec-related examples, including KMP and several QCP demo relation proofs.

🧩 New glibc Singly Linked List Verification Suite

• Added a new glibc-style singly linked list verification suite under QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel.
• The suite includes 16 relation examples covering append, copy, free, iteration, merge, reverse, multi-list operations, and tail/list append variants.
• Added the corresponding Rocq goals, auto proofs, manual proofs, local libraries, and goal checks under SeparationLogic/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel.

📚 New Graph and Algorithm Libraries

• Added SeparationLogic/algorithms, covering BFS, DFS, Dijkstra, Floyd, Kruskal, Prim, Tarjan, and supporting proof infrastructure.
• Expanded GraphLib with additional graph basics, reachability/path utilities, BFS distance support, subgraph reasoning, rooted trees, and undirected tree developments.
• Added MaxMinLib/Interface.v and supporting list-library lemmas.

Improvements

• Vendored tracelib and coq-record-update into the repository source tree to make the proof environment more self-contained.
• Improved proof hygiene documentation, including clearer rules for forbidden lemmas, helper migration, and final checks.
• Repaired proof scripts and local libraries affected by updated forbidden-lemma rules and generated VC changes.
• Cleaned up minigmp_sumlib manual proofs after the SumLib migration.

Migration Notes

• When refreshing C examples, keep C header search paths (-I) and Rocq logical-path mappings (-slp) both correctly configured; they serve different purposes and are not interchangeable.
• Regenerated VCs may change witness numbering, branch order, and PreH hypothesis names. Manual proofs should be repaired by reading the current *_goal.v and matching the semantic postcondition, not by copying old witness numbers.
• If a witness is already proved by *_proof_auto.v, it should not be duplicated in *_proof_manual.v.
• Safeexec relation examples should use the updated Hoare_safeexec_compose-based flow and should not reintroduce removed equiv or direct program_equiv obligations.

---

We appreciate your feedback! Please report any issues on our issue tracker or contact the team directly.

Happy verifying with QCP v2.0.3!