QualifiedCProgramming: Skill for Claude Code

Annotation Design and Authoring

One annotation owner handles the initial attempt and every retry in the main root.

Work in this order:

problem statement
  -> natural-language specification
  -> Rocq specification
  -> C function contract
  -> loop invariant
  -> symexec

The natural-language specification, Rocq Spec, and C Ensure state the same output relation. Editorials, algorithm hints, loop state, DP transitions, and data-structure construction do not belong in the top-level specification.

Before writing a definition, search the current dependencies, canonical case library, and shared libraries. Directly combine existing predicates such as Zlength, Znth, sublist, replace_Znth, Forall, Forall2, In, NoDup, Permutation, sum, and the existing monotonicity, extrema, path, and array predicates. Do not add successive wrappers around those combinations. When the problem meaning or a cross-function interface needs a name, keep one case predicate and refer to it directly everywhere else.

Result and progress predicates contain mathematics only, without memory ownership, input restrictions, or implementation-safety ranges. Retain the candidate sets, valid domains, and output formats needed to define the answer. Expand input ranges, element ranges, and overflow conditions in the function contract. Use With for logical values and Require for entry conditions and resources. The mathematical part of Ensure promises only the required final result; return spatial resources separately.

Use Z and Z-indexed list interfaces in new specifications, helpers, and annotations, and Forall for index-independent elementwise properties. Extrema must use MaxMinLib's min_value_of_subset / max_value_of_subset. Reuse sum_range / sum / sum_set_R for sums, Zrange for range enumeration, clos_refl_trans for reflexive-transitive closure, Veci / Vecp / VecpArray for growable vectors, and CDCLLib's literal / clause / cnf / models / cnf_sat / cnf_unsat for CNF and SAT; do not redefine these meanings. See the knowledge rules for boundaries, signatures, and examples.

Put one Inv Assert before every loop. It contains only mathematical progress, ranges needed by the next execution step, live resources, and necessary @pre bridges. Use an ordinary Assert only when symbolic execution cannot recover state needed downstream; it may appear before an if, but not before a return or an Inv Assert. Do not use by local, branch control, ordinary Inv, multi-invariants, or call where clauses in a function body.

Keep a user-provided specification unchanged. If it must change, describe the function, reason, edit, and semantic change in agent_output.md and return it to main. Continue in the same attempt after user approval and unfreeze.