doc: add coding guidelines

AGENTS.md

@@ -22,23 +22,10 @@ This repository contains the Verus proof development for Asterinas OSTD. The lay
 - `make doc`: verify and generate API documentation in `doc/`.
 - `make clean`: remove Cargo and generated documentation artifacts.
 
-## Coding Style & Naming Conventions
-
-- Use Rust 2021 style with Verus proof conventions.
-- Keep executable code, `spec` functions, proof blocks, and lemmas clearly separated so verification intent is visible in review.
-- Name modules and files in `snake_case`; use `CamelCase` for types and traits, `SCREAMING_SNAKE_CASE` for constants, prefix proof lemmas using `lemma_` like `lemma_page_table_mapping_preserved`, prefix axioms using `axiom_`, and prefix `tracked_` for helper functions that lift verus functions that return ghost types into `tracked`.
-- Formatting follows `rustfmt.toml`: 4-space indentation, crate-level import grouping, and reordered imports.
-- Public verified APIs should include rustdoc comments explaining both behavior and proof obligations. Suppress lints at the narrowest practical scope, preferably with `#[expect(...)]`.
-- Whenever there is proof-only objects inside executable Rust types, be sure to add prefixes to the variables. Example:
-  ```rs
-  pub struct Foo {
-      something: u64,
-      tracked_thing: Tracked<u8>,
-      //             ^^^^^^^
-      ghost_another: Ghost<u32>,
-      //             ^^^^^
-  }
-  ```
+## Coding Guidelines
+
+Follow the [VOSTD Verus Coding Guidelines](docs/coding-guidelines/README.md)
+for coding, specification, proof, naming, and review conventions.
 
 ## Verus Requirements
 

docs/README.md

@@ -0,0 +1,4 @@
+# VOSTD Documentation
+
+- [Verus Coding Guidelines](coding-guidelines/README.md) — conventions for
+  writing and reviewing VOSTD specifications and proofs.

docs/coding-guidelines/README.md

@@ -0,0 +1,43 @@
+# VOSTD Verus Coding Guidelines
+
+These guidelines combine established repository policy and recurring VOSTD
+review feedback into a shared standard for writing and reviewing Verus
+specifications and proofs. They complement, rather than replace, the operational
+rules in `AGENTS.md` and the Verus documentation.
+
+Use Rust 2021 style and run the project formatter. Formatting follows
+`rustfmt.toml`, including four-space indentation, crate-level import grouping,
+and reordered imports; these mechanically enforced rules are not repeated as
+individual guidelines.
+
+Each guideline has a stable kebab-case short name. Use that name in reviews so
+that a comment can link to the rule instead of restating it.
+
+## Guidelines
+
+### Proof engineering
+
+- [`complete-external-contracts`](proof-engineering.md#complete-external-contracts) — model every relevant precondition, result, frame condition, and panic behavior at an external boundary.
+- [`centralize-trusted-boundaries`](proof-engineering.md#centralize-trusted-boundaries) — keep unavoidable external specifications in `vstd_extra::external` and make their trust explicit.
+- [`reuse-existing-specifications`](proof-engineering.md#reuse-existing-specifications) — check `vstd` and existing project models before introducing a new abstraction.
+- [`canonical-spec-models`](proof-engineering.md#canonical-spec-models) — use the simplest standard mathematical model that preserves the API semantics.
+- [`implement-inv-for-models`](proof-engineering.md#implement-inv-for-models) — implement `Inv` for intrinsic model invariants that Verus cannot enforce as type invariants.
+
+### Maintainability
+
+- [`separate-verus-modes`](maintainability.md#separate-verus-modes) — keep executable code, specifications, and proofs visually distinct.
+- [`preserve-exec-code`](maintainability.md#preserve-exec-code) — preserve executable code and source layout while adding proofs.
+- [`name-proof-roles`](maintainability.md#name-proof-roles) — name proof functions and resources after their proof and ownership roles.
+- [`avoid-redundant-mode-markers`](maintainability.md#avoid-redundant-mode-markers) — do not add `ghost` or `tracked` markers where the enclosing mode already determines the value's role.
+- [`document-verified-apis`](maintainability.md#document-verified-apis) — document both runtime behavior and proof obligations on public verified APIs.
+- [`narrow-lint-suppressions`](maintainability.md#narrow-lint-suppressions) — suppress a lint only at the smallest scope that requires it.
+- [`right-size-spec-placement`](maintainability.md#right-size-spec-placement) — keep small local models near their implementation unless they form a reusable subsystem.
+- [`document-real-proof-debt`](maintainability.md#document-real-proof-debt) — keep proof comments tied to real source constraints and mark unresolved boundaries explicitly.
+- [`qualified-verus-spec-calls`](maintainability.md#qualified-verus-spec-calls) — use qualified paths where `#[verus_spec]` attaches a specification to a call.
+
+### Workflow
+
+- [`verify-across-supported-hosts`](workflow.md#verify-across-supported-hosts) — treat host-dependent verification results as a proof robustness problem.
+- [`decompose-before-raising-rlimit`](workflow.md#decompose-before-raising-rlimit) — localize and simplify unstable proofs before increasing solver resource limits.
+- [`upstream-reusable-specs`](workflow.md#upstream-reusable-specs) — contribute generally useful standard-library specifications upstream after validating them in VOSTD.
+- [`preserve-toolchain-configurations`](workflow.md#preserve-toolchain-configurations) — isolate toolchain-specific proofs and verify every supported configuration.

docs/coding-guidelines/maintainability.md

@@ -0,0 +1,171 @@
+# Maintainability
+
+### Separate Verus modes
+
+<!-- guideline: separate-verus-modes -->
+
+Keep executable code, `spec` functions, proof blocks, and reusable lemmas
+visually distinct. A reviewer should be able to see which code runs, which code
+defines the mathematical model, and which code exists only to establish a
+proof.
+
+Prefer small, coherent groups over interleaving mode changes throughout an
+implementation. Keep adjacent verified items in the same `verus!` block when
+no ordinary Rust item separates them.
+
+### Preserve exec code
+
+<!-- guideline: preserve-exec-code -->
+
+Add specifications and proofs without rewriting executable Rust or moving its
+items. If Verus requires a different executable expression, keep the change
+minimal, demonstrate that runtime behavior is unchanged, and make the original
+form visible in review.
+
+This includes preserving import-independent item order: proof migration should
+not move constants, methods, or module declarations merely to make a partial
+file compile.
+
+See also: PR [#692](https://github.com/asterinas/vostd/pull/692#discussion_r3720382959),
+[#692](https://github.com/asterinas/vostd/pull/692#discussion_r3720371945), and
+[#674](https://github.com/asterinas/vostd/pull/674#discussion_r3664166187).
+
+### Name proof roles
+
+<!-- guideline: name-proof-roles -->
+
+Use `snake_case` for modules and files, `CamelCase` for types and traits, and
+`SCREAMING_SNAKE_CASE` for constants. Prefix proved reusable facts with
+`lemma_`, axioms with `axiom_`, and helpers that manipulate tracked variables
+with `tracked_`. Name resources after the ownership role they
+represent, especially when several resources belong to the same protocol.
+
+```rust
+proof fn lemma_mapping_preserved(...) { ... }
+proof fn tracked_borrow(...) -> (...) { ... }
+```
+
+Avoid broad names such as `CpuCore` or indistinguishable protocol resource names
+when the type actually represents a specific authority, owner, pool, or state.
+
+See also: PR [#679](https://github.com/asterinas/vostd/pull/679#discussion_r3690850716),
+[#723](https://github.com/asterinas/vostd/pull/723#discussion_r3849117460),
+[#723](https://github.com/asterinas/vostd/pull/723#issuecomment-5392419977), and
+[#672](https://github.com/asterinas/vostd/pull/672#issuecomment-5099747820).
+
+### Avoid redundant mode markers
+
+<!-- guideline: avoid-redundant-mode-markers -->
+
+Use `ghost` and `tracked` markers where they communicate or enforce a mode
+boundary. Prefix proof-only fields inside executable types with `ghost_` or
+`tracked_` so their erasure and ownership role are visible:
+
+```rust
+pub struct Foo {
+    value: u64,
+    tracked_permission: Tracked<Permission>,
+    ghost_model: Ghost<Model>,
+}
+```
+
+Do not repeat the marker on every field of a `ghost struct`.
+For a `tracked struct`, fields are `tracked` by default,
+so we need to add `ghost` marker to fields that are not linear ownerships.
+
+See also: PR [#703](https://github.com/asterinas/vostd/pull/703#discussion_r3763958841).
+
+### Document verified APIs
+
+<!-- guideline: document-verified-apis -->
+
+Preserve the original runtime documentation. Add rustdoc for every public
+verified API and for proof functions or modules whose properties are important
+to callers or proof maintainers.
+
+Describe preconditions, postconditions, and invariants in natural language. The
+documentation need not correspond one-to-one with every Verus clause, but it
+must cover the critical properties and be understandable to kernel developers
+without requiring Verus knowledge.
+
+For a public executable API, add a `Verified Properties` section after its
+original documentation. Include:
+
+- `Safety`: State the classes of undefined behavior that have been ruled out
+  and identify any remaining trusted boundaries. Do not claim the absence of
+  all undefined behavior unless that claim is justified.
+- `Functional Correctness`, when applicable: Summarize the behavior established
+  by verification.
+- `Preconditions`: Explain the obligations that callers must satisfy.
+- `Postconditions`: Explain the properties guaranteed on return, including
+  whether the function cannot panic when this has been proved.
+
+For a proof function, begin with one sentence summarizing the fact being proved,
+followed by `Preconditions` and `Postconditions` sections that explain the
+important proof clauses.
+
+For a verified module, add a `Verified Properties` section describing its
+verification design, critical invariants, safety properties, and any verified
+functional-correctness properties.
+
+Do not merely restate signatures or Verus expressions. Record the information a
+caller needs to use the API without reading its implementation or proof.
+
+See also:
+[`SpinLock`](../../ostd/src/sync/spin.rs#L18),
+[`AlignExt`](../../ostd/libs/align_ext/src/lib.rs#L98), and
+[`entails_and_temp_reverse`](../../verified_libs/vstd_extra/src/temporal_logic/rules.rs#L793).
+
+### Narrow lint suppressions
+
+<!-- guideline: narrow-lint-suppressions -->
+
+Suppress a lint at the smallest item or expression that requires it. Prefer
+`#[expect(...)]` when the lint is deliberately triggered so that the compiler
+can report when the suppression becomes obsolete.
+
+Avoid crate- or module-wide allowances for a local Verus interoperability issue.
+
+### Right-size spec placement
+
+<!-- guideline: right-size-spec-placement -->
+
+Keep a small, implementation-specific model beside its verified code. Create a
+separate file under `ostd/specs/` when the model is substantial, shared, or
+expected to grow into a subsystem-level interface.
+
+File placement should reduce navigation cost; it should not mechanically split
+a short model from its only user.
+
+See also: PR [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3740708147)
+and [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3740719198).
+
+### Document real proof debt
+
+<!-- guideline: document-real-proof-debt -->
+
+Keep comments that explain a current proof boundary, non-obvious invariant, or
+known missing model. Add a `TODO` when a temporary limitation needs follow-up.
+Do not copy explanatory comments that are absent from the executable source or
+retain comments after the condition they describe is removed.
+
+See also: PR [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3820204595)
+and [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3819464685).
+
+### Qualified Verus spec calls
+
+<!-- guideline: qualified-verus-spec-calls -->
+
+When attaching `#[verus_spec]` to a function call, use a qualified path if name
+resolution through an import prevents Verus from finding the specification.
+
+```rust
+let slot = (#[verus_spec(with Tracked(slot_perm))]
+    crate::mm::frame::meta::get_slot(frame));
+```
+
+Prefer this local, explicit workaround over adding an import solely to change
+how the attribute resolves the callee.
+
+See also: PR [#673](https://github.com/asterinas/vostd/pull/673#discussion_r3662337926)
+and [#673](https://github.com/asterinas/vostd/pull/673#discussion_r3662532282).

docs/coding-guidelines/proof-engineering.md

@@ -0,0 +1,99 @@
+# Proof Engineering
+
+### Complete external contracts
+
+<!-- guideline: complete-external-contracts -->
+
+An external specification must state every caller obligation and every semantic
+fact on which a proof relies: preconditions, postconditions, well-formedness, and panic behavior.
+
+For example, a `BTreeMap::get_mut` model must preserve entries other than the
+selected key and must express the documented compatibility between the stored
+key ordering and borrowed-key ordering. A potentially panicking function must
+not be specified as `no_unwind`.
+
+See also: PR [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3747054386),
+[#699](https://github.com/asterinas/vostd/pull/699#discussion_r3763419050), and
+[#692](https://github.com/asterinas/vostd/pull/692#discussion_r3732701232).
+
+### Centralize trusted boundaries
+
+<!-- guideline: centralize-trusted-boundaries -->
+
+Put an unavoidable specification for an opaque `core`, `alloc`, or `std` API in
+the appropriate module under `verified_libs/vstd_extra/src/external/`. Do not
+hide a local assumption beside an OSTD caller, and do not treat relocation as a
+proof of soundness.
+
+Every unsafe external helper needs contracts strong enough to justify its
+callers. Delete an unused helper instead of retaining an unconstrained trusted
+boundary.
+
+See also: PR [#674](https://github.com/asterinas/vostd/pull/674#discussion_r3671555470),
+[#674](https://github.com/asterinas/vostd/pull/674#discussion_r3687737109), and
+[#703](https://github.com/asterinas/vostd/pull/703#issuecomment-5264921275).
+
+### Reuse existing specifications
+
+<!-- guideline: reuse-existing-specifications -->
+
+Before adding a helper, axiom, or external specification, search the active
+`vstd` and `vstd_extra` APIs. Use the existing verified operation directly when
+it already carries the required semantics.
+
+```rust
+// Prefer an existing spec-enabled operation.
+let result = lhs.saturating_add(rhs);
+
+// Avoid a duplicate wrapper with an equivalent contract.
+```
+
+If existing support is incomplete, extend it at the narrowest reusable layer
+instead of creating overlapping local models.
+
+See also: PR [#699](https://github.com/asterinas/vostd/pull/699#issuecomment-5225757765),
+[#692](https://github.com/asterinas/vostd/pull/692#discussion_r3733886308), and
+[#699](https://github.com/asterinas/vostd/pull/699#discussion_r3763403672).
+
+### Canonical spec models
+
+<!-- guideline: canonical-spec-models -->
+
+Choose the simplest standard mathematical type that faithfully represents the
+executable value. Prefer `Range<int>` for an integer range, `Map` for a map
+view, and a sequence plus a position for an ordered cursor when those models
+capture the required semantics directly.
+
+Make type-level properties independent of irrelevant value arguments, and make
+predicates methods when they describe the well-formedness of one model.
+
+See also: PR [#703](https://github.com/asterinas/vostd/pull/703#discussion_r3763971349),
+[#704](https://github.com/asterinas/vostd/pull/704#issuecomment-5265438143),
+[#704](https://github.com/asterinas/vostd/pull/704#discussion_r3809917573), and
+[#704](https://github.com/asterinas/vostd/pull/704#discussion_r3767737737).
+
+### Implement Inv for models
+
+<!-- guideline: implement-inv-for-models -->
+
+When a spec-level model has an intrinsic validity invariant, implement the
+`Inv` trait and define it through `inv()`:
+
+```rust
+impl Inv for Model {
+    open spec fn inv(self) -> bool {
+        // The model invariant.
+    }
+}
+```
+
+Require `inv()` before operations that assume a valid state and ensure it after
+operations that promise to preserve validity. For mutable operations, state
+this as `old(self).inv()` and `final(self).inv()` where appropriate.
+
+Use a separate `wf(...)` predicate only for well-formedness relationships that
+depend on another value. Making fields private provides representation hiding;
+it does not cause Verus to establish `inv()` automatically.
+
+See also: PR [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3801496837)
+and [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3810349440).