Development guide

Read the architecture guide for the meaning of the final theorem and the relationship between concrete code, abstract operations, invariants, and proofs. This guide describes how to navigate and extend that existing structure.

Reproduce the toolchain

The migration was checked with Rocq 9.2.0, Stdlib 9.1.0, and OCaml 5.4.0 on Apple Silicon macOS. With opam already initialized, prepare an independent switch as follows:

opam switch create certiucos2 ocaml-base-compiler.5.4.0
opam install --switch=certiucos2 rocq-core.9.2.0 rocq-stdlib.9.1.0
eval "$(opam env --switch=certiucos2 --set-switch)"

You also need make and Python 3; the latter runs the assumption audit. From the repository root:

make version
make -j2
make check
make audit

scripts/rocq.sh selects CERTIUCOS_ROCQ when set, then rocq from PATH, then the existing sibling Iris/vsimpler environment on the migration machine. That sibling checkout is a local convenience, not a project dependency. An independent switch needs the packages above, not the Iris project.

make discovers proof sources under coqimp/framework, coqimp/tactics, and coqimp/certiucos; rocq dep generates their dependency graph. There is no hand-maintained list of .v files to update. make check first brings the objects up to date and then recursively checks all modules with rocq check. make audit compares source declarations with the upstream baseline and checks for admitted proofs and known kernel-check bypasses. It is a source regression check, not a proof that the baseline assumptions are consistent.

Use one or two compilation jobs on a machine with 16 GiB of RAM. Some API proofs and final proof-term checks need substantial memory. Do not start several independent builds against the same checkout: they can overwrite the same .vo files while other compilers consume them.

After changing the toolchain, or for a release verification, run these as separate commands:

make clean
make -j2
make check
make audit

The clean step removes generated proof objects and dependency files. The uCert-code C/assembly tree is outside this proof build.

Work on a small proof target first

Use make for a single target so that prerequisite modules are rebuilt:

make -C coqimp -j2 certiucos/proofs/msgqueue/OSQAcceptProof.vo
make -C coqimp -j2 certiucos/proofs/ucos_correct.vo

For a diagnostic compile after dependencies are current:

cd coqimp
../scripts/rocq.sh compile -time -R . CertiOS certiucos/proofs/msgqueue/OSQAcceptProof.v

The -time output helps distinguish a slow tactic from a slow final Qed. The direct command does not rebuild imports. After a shared dependency changes, return to make instead of compiling consumers against stale objects. coqimp/_CoqProject supplies the -R . CertiOS mapping for editor integrations; configure the editor to use the same Rocq switch as the command line.

Useful source searches from the repository root include:

rg -n 'OSQAccept_impl|api_fun_list' coqimp/certiucos/code
rg -n 'qaccapi|qacc_absinfer' coqimp/certiucos/spec
rg -n 'OSQAccProof|ucos_toprule' coqimp/certiucos/proofs
rg -n 'Definition OS_spec|Definition os_spec' coqimp/certiucos/spec

Add or change a kernel API

Start from an existing API with similar resource and scheduling behavior. OSQAccept is a compact example of a nonblocking operation; a blocking API also needs the relevant wait-list, scheduler, and interrupt interactions. The following steps are a workflow, not a claim that every change needs a new definition in every file.

Specify the behavior and identify the state. Write down argument and result types, failure cases, abstract state changes, and any scheduling or blocking points. Inspect abs_op.v and the existing invariant predicates before choosing a representation. Include invalid/null inputs when they are part of the modeled API's behavior.
Define the modeled implementation. Add or reuse identifiers in certiucos/code/os_code_defs.v, and structures/constants in os_ucos_h.v when needed. Put the function term in the appropriate os_*.v module using code_notations.v. Register an externally callable implementation in os_program.v's api_fun_list. A new internal helper belongs in internal_fun_list; interrupt handlers belong in interrupt_list. Keep identifiers distinct: the conversion functions search lists in order, so a duplicate identifier can hide a later entry.
Define and register the abstract operation. In abs_op.v, express the permitted abstract transitions and combine their cases into specification code. Pair that code with its result/argument signature, as qaccapi does. Add the same function identifier and specification to os_spec.v's api_spec_list. Interrupt specifications use int_spec_list. Check that concrete and abstract signatures agree.
Prove the abstract-step rules. Add checked lemmas in the appropriate spec/absoprules module. These should justify the transitions used by the concrete proof, preserving framed resources. Reuse existing rules when the abstract operation is unchanged.
Account for invariants and internal contracts. Reuse OSInv, OSLInv, the task/event relations, and bitmap/list predicates where possible. If a shared representation changes, update its invariant and preservation lemmas in os_inv.v, inv_prop.v, new_inv.v, and the affected ucos_lib modules as required by their actual dependencies. A new internal helper additionally needs pre/postconditions in ifun_spec.v, GoodFunAsrt proofs, a signature, and an entry in its osq_spec_list table. Public API abstract operations and these internal Hoare contracts serve different purposes.
Prove the body. Put reusable data-structure facts in ucos_lib and the implementation theorem in the corresponding proofs family. Follow the existing theorem interface: API proofs consume BuildPreA' and BuildRetA' and return the registered body plus its InfRules derivation. Internal helpers and interrupt handlers use their corresponding interfaces. Restore the appropriate invariant at each boundary required by the rules; account explicitly for abstract transitions and scheduling.
Integrate the result. Import the theorem into proofs/ucos_correct.v. Extend the case analysis in ucos_toprule and the affected domain, signature, declaration, and call-discipline lemmas. A standalone theorem does not automatically extend ucos_correct: the registration tables and integration proof must cover it.
Validate the whole dependency chain. Compile the local target, then ucos_correct.vo, then every source with make, and run make check and make audit. A changed shared invariant can affect distant APIs. Document any deliberate change to a theorem statement or supported behavior.

Where the proof automation lives

ucos_include.v is the common OS-proof import bundle. It brings together the specifications, framework, and automation. Add a direct import for an API-specific helper that it does not export; avoid introducing import cycles merely to obtain a convenient lemma.

Typical task	Entry points
Advance modeled statements and function calls	`tactics/hoare_forward.v`, `hoareforward/`, and `ucostac/ucos_forward.v`
Rearrange and discharge separation assertions	`tactics/sep_auto.v` and `sepauto/`
Advance abstract specification code	`tactics/abs_step.v` and `absstep/`, together with `spec/absoprules/`
Prove map joins and updates	`tactics/basetac/` and `framework/auxlibs/Modules.v`
Solve integer, bitmap, and structural side conditions	`tactics/math_auto.v`, `mathauto/`, `pure/`, and `ucostac/ucos_bitsmap.v`
Reuse an inline implementation proof	`certiucos/inline/`

Read a failed goal before adding more automation. Modern Rocq can change generated hypothesis names and solve a side condition earlier than an old script expected. Prefer explicit arguments when inference selects the wrong witness, and structural matches or named hypotheses over fixed H123 names. Scope a side-condition script to the goal it is meant to solve; a standalone clear after a tactic that already closed its goal can accidentally erase facts from the next goal. If a tactic unexpectedly becomes expensive, inspect the first unresolved constructor disequality, arithmetic bound, or existential witness instead of broadly increasing search depth.

Preserve the verification boundary

Normal maintenance must not add axioms, admitted lemmas, skipped proof checks, or assumption changes to make a build pass. Do not replace a failed Qed with Admitted, use .vos/quick compilation as completion evidence, or disable guard, positivity, or universe checking. Historical Abort commands are recorded by the audit; they discard proofs and do not supply missing theorems. Do not add new ones to conceal unfinished required work.

Preserve theorem statements during a compatibility-only change. Keep compatibility aliases in framework/auxlibs/LegacyArith.v backed by existing definitions or checked proofs. Do not hide migration diagnostics by suppressing all warnings; some compatibility failures require real declaration or proof repairs.

The existing MemoryNotFull assumption is inconsistent with the unrestricted memory-map model, as explained in the architecture guide. Extending this project does not remove that caveat. Repairing it requires an explicitly scoped model change, updated dependent proofs, and a reviewed trust record; editing the baseline JSON to silence an audit is not a repair.

rocq-verification.json records a specific checked source snapshot, including raw source hashes. Even a comment edit changes those hashes. Keep the checked record and the current source revision clearly distinguished, and regenerate verification evidence after completing the corresponding checks rather than changing recorded success results by hand.