From e784ffd5a185d0d2600782604cf128d5f9cc2d1a Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 26 Aug 2026 19:10:52 +0800 Subject: [PATCH 1/2] doc: add coding guidelines --- AGENTS.md | 21 +-- docs/README.md | 4 + docs/coding-guidelines/README.md | 44 ++++++ docs/coding-guidelines/maintainability.md | 142 ++++++++++++++++++++ docs/coding-guidelines/proof-engineering.md | 105 +++++++++++++++ docs/coding-guidelines/workflow.md | 66 +++++++++ 6 files changed, 365 insertions(+), 17 deletions(-) create mode 100644 docs/README.md create mode 100644 docs/coding-guidelines/README.md create mode 100644 docs/coding-guidelines/maintainability.md create mode 100644 docs/coding-guidelines/proof-engineering.md create mode 100644 docs/coding-guidelines/workflow.md diff --git a/AGENTS.md b/AGENTS.md index b533d334b..246a10799 100644 --- a/AGENTS.md +++ b/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, - // ^^^^^^^ - ghost_another: Ghost, - // ^^^^^ - } - ``` +## Coding Guidelines + +Follow the [VOSTD Verus Coding Guidelines](docs/coding-guidelines/README.md) +for coding, specification, proof, naming, and review conventions. ## Verus Requirements diff --git a/docs/README.md b/docs/README.md new file mode 100644 index 000000000..11b93f7ec --- /dev/null +++ b/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. diff --git a/docs/coding-guidelines/README.md b/docs/coding-guidelines/README.md new file mode 100644 index 000000000..347f5a43d --- /dev/null +++ b/docs/coding-guidelines/README.md @@ -0,0 +1,44 @@ +# 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. +- [`explicit-well-formedness`](proof-engineering.md#explicit-well-formedness) — expose and preserve well-formedness when Verus cannot enforce it as a type invariant. +- [`choose-proof-resource-by-scope`](proof-engineering.md#choose-proof-resource-by-scope) — use a tokenized state machine only when the modeled subsystem is sufficiently self-contained. + +### 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. diff --git a/docs/coding-guidelines/maintainability.md b/docs/coding-guidelines/maintainability.md new file mode 100644 index 000000000..89b511ab8 --- /dev/null +++ b/docs/coding-guidelines/maintainability.md @@ -0,0 +1,142 @@ +# Maintainability + +### 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 + + + +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 + + + +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 lift ghost-returning operations +into tracked mode 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 + + + +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, + ghost_model: Ghost, +} +``` + +Do not repeat the marker on every field of an already ghost-only struct, and do +not declare a value `tracked` unless it carries linear proof state that requires +tracked handling. + +See also: PR [#703](https://github.com/asterinas/vostd/pull/703#discussion_r3763958841). + +### Document verified APIs + + + +Add rustdoc to public verified APIs that explains both runtime behavior and the +proof contract. Describe the meaning of important `requires` and `ensures` +clauses, ownership transferred through tracked arguments or results, and any +trusted boundary on which callers rely. + +Do not merely restate the function signature. Record the information a caller +needs to use the API without reading its proof. + +### 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 + + + +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 + + + +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 + + + +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). diff --git a/docs/coding-guidelines/proof-engineering.md b/docs/coding-guidelines/proof-engineering.md new file mode 100644 index 000000000..032303f51 --- /dev/null +++ b/docs/coding-guidelines/proof-engineering.md @@ -0,0 +1,105 @@ +# Proof Engineering + +### Complete external contracts + + + +An external specification must state every caller obligation and every semantic +fact on which a proof relies: preconditions, postconditions, frame conditions, +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 + + + +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 + + + +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 + + + +Choose the simplest standard mathematical type that faithfully represents the +executable value. Prefer `Range` 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). + +### Explicit well-formedness + + + +When a spec-level ghost model cannot use `#[verifier::type_invariant]`, expose a +clear `wf()` predicate and carry it explicitly through operation contracts. +Require well-formedness before an operation and ensure it afterward whenever +the API promises that the state remains valid. + +Do not make fields private under the assumption that representation hiding will +cause Verus to establish an invariant 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). + +### Choose proof resource by scope + + + +Use a tokenized state machine when the verified subsystem is self-contained and +its internal state transitions define the relevant behavior. Prefer composable +permissions or resource algebras when ownership must cross subsystem boundaries +or evolve with loosely coupled kernel components. + +Decide from the verification goal and expected composition boundaries, not from +the convenience of encoding the first local transition. + +See also: PR [#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5163134765), +[#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5163188523), and +[#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5189197277). diff --git a/docs/coding-guidelines/workflow.md b/docs/coding-guidelines/workflow.md new file mode 100644 index 000000000..0f2d6b6e4 --- /dev/null +++ b/docs/coding-guidelines/workflow.md @@ -0,0 +1,66 @@ +# Verification Workflow + +### Verify across supported hosts + + + +A proof that succeeds on one supported host but fails on another is not stable. +Run the repository verification gate and the configured Linux/macOS checks for +proof-sensitive changes, especially after a Verus, Z3, or target-architecture +update. + +Treat platform-dependent quantifier instantiation or resource-limit behavior as +evidence that the proof needs localization, even when one CI job happens to +pass. + +See also: PR [#688](https://github.com/asterinas/vostd/pull/688#issuecomment-5174118963) +and [#674](https://github.com/asterinas/vostd/pull/674#issuecomment-5143566443). + +### Decompose before raising rlimit + + + +When a proof times out or becomes solver-version-sensitive, first split a large +proof into smaller lemmas, remove irrelevant context, and make quantifier use +more explicit. Increase `#[verifier::rlimit(...)]` only when the localized proof +still has a justified resource requirement. + +An `rlimit` increase can be a temporary compatibility measure during a solver +upgrade, but it should remain visible as proof debt and should not replace proof +simplification. + +See also: PR [#688](https://github.com/asterinas/vostd/pull/688#issuecomment-5174425113), +[#678](https://github.com/asterinas/vostd/pull/678#issuecomment-5139803494), and +[#681](https://github.com/asterinas/vostd/pull/681#issuecomment-5151453444). + +### Upstream reusable specs + + + +When VOSTD develops a generally useful specification for a standard-library +API, validate it against a real VOSTD caller and then propose it to upstream +Verus. Keep the temporary `vstd_extra` model narrowly scoped so that it can be +removed when upstream support lands. + +Discuss fundamental missing models, such as the semantics of `Borrow`, with +Verus maintainers before cementing a project-local axiom around them. + +See also: PR [#699](https://github.com/asterinas/vostd/pull/699#discussion_r3747182992), +[#704](https://github.com/asterinas/vostd/pull/704#issuecomment-5265453465), and +[#699](https://github.com/asterinas/vostd/pull/699#issuecomment-5354033977). + +### Preserve toolchain configurations + + + +Proofs that depend on a toolchain branch or experimental memory model must be +isolated behind an explicit configuration. Preserve the default verification +path and verify both the default and experimental configurations in separate CI +jobs. + +Keep project-specific toolchain patches in the project fork only when they are +not appropriate as independent upstream changes; record where they came from +and which configuration needs them. + +See also: PR [#708](https://github.com/asterinas/vostd/pull/708#issuecomment-5290616590) +and [#708](https://github.com/asterinas/vostd/pull/708#issuecomment-5290899675). From af3406cffc8500b06116606fc17c86d7d5d13c44 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 27 Aug 2026 18:42:12 +0800 Subject: [PATCH 2/2] doc: refine according to review --- docs/coding-guidelines/README.md | 3 +- docs/coding-guidelines/maintainability.md | 53 ++++++++++++++++----- docs/coding-guidelines/proof-engineering.md | 46 ++++++++---------- docs/coding-guidelines/workflow.md | 4 +- 4 files changed, 65 insertions(+), 41 deletions(-) diff --git a/docs/coding-guidelines/README.md b/docs/coding-guidelines/README.md index 347f5a43d..5a3a2d496 100644 --- a/docs/coding-guidelines/README.md +++ b/docs/coding-guidelines/README.md @@ -21,8 +21,7 @@ that a comment can link to the rule instead of restating it. - [`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. -- [`explicit-well-formedness`](proof-engineering.md#explicit-well-formedness) — expose and preserve well-formedness when Verus cannot enforce it as a type invariant. -- [`choose-proof-resource-by-scope`](proof-engineering.md#choose-proof-resource-by-scope) — use a tokenized state machine only when the modeled subsystem is sufficiently self-contained. +- [`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 diff --git a/docs/coding-guidelines/maintainability.md b/docs/coding-guidelines/maintainability.md index 89b511ab8..288bcb747 100644 --- a/docs/coding-guidelines/maintainability.md +++ b/docs/coding-guidelines/maintainability.md @@ -36,8 +36,8 @@ See also: PR [#692](https://github.com/asterinas/vostd/pull/692#discussion_r3720 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 lift ghost-returning operations -into tracked mode with `tracked_`. Name resources after the ownership role they +`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 @@ -69,9 +69,9 @@ pub struct Foo { } ``` -Do not repeat the marker on every field of an already ghost-only struct, and do -not declare a value `tracked` unless it carries linear proof state that requires -tracked handling. +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). @@ -79,13 +79,42 @@ See also: PR [#703](https://github.com/asterinas/vostd/pull/703#discussion_r3763 -Add rustdoc to public verified APIs that explains both runtime behavior and the -proof contract. Describe the meaning of important `requires` and `ensures` -clauses, ownership transferred through tracked arguments or results, and any -trusted boundary on which callers rely. - -Do not merely restate the function signature. Record the information a caller -needs to use the API without reading its proof. +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 diff --git a/docs/coding-guidelines/proof-engineering.md b/docs/coding-guidelines/proof-engineering.md index 032303f51..183443040 100644 --- a/docs/coding-guidelines/proof-engineering.md +++ b/docs/coding-guidelines/proof-engineering.md @@ -5,8 +5,7 @@ An external specification must state every caller obligation and every semantic -fact on which a proof relies: preconditions, postconditions, frame conditions, -well-formedness, and panic behavior. +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 @@ -73,33 +72,28 @@ See also: PR [#703](https://github.com/asterinas/vostd/pull/703#discussion_r3763 [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3809917573), and [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3767737737). -### Explicit well-formedness +### Implement Inv for models - + -When a spec-level ghost model cannot use `#[verifier::type_invariant]`, expose a -clear `wf()` predicate and carry it explicitly through operation contracts. -Require well-formedness before an operation and ensure it afterward whenever -the API promises that the state remains valid. +When a spec-level model has an intrinsic validity invariant, implement the +`Inv` trait and define it through `inv()`: -Do not make fields private under the assumption that representation hiding will -cause Verus to establish an invariant 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). - -### Choose proof resource by scope - - +```rust +impl Inv for Model { + open spec fn inv(self) -> bool { + // The model invariant. + } +} +``` -Use a tokenized state machine when the verified subsystem is self-contained and -its internal state transitions define the relevant behavior. Prefer composable -permissions or resource algebras when ownership must cross subsystem boundaries -or evolve with loosely coupled kernel components. +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. -Decide from the verification goal and expected composition boundaries, not from -the convenience of encoding the first local transition. +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 [#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5163134765), -[#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5163188523), and -[#683](https://github.com/asterinas/vostd/pull/683#issuecomment-5189197277). +See also: PR [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3801496837) +and [#704](https://github.com/asterinas/vostd/pull/704#discussion_r3810349440). diff --git a/docs/coding-guidelines/workflow.md b/docs/coding-guidelines/workflow.md index 0f2d6b6e4..20d31dc44 100644 --- a/docs/coding-guidelines/workflow.md +++ b/docs/coding-guidelines/workflow.md @@ -23,7 +23,9 @@ and [#674](https://github.com/asterinas/vostd/pull/674#issuecomment-5143566443). When a proof times out or becomes solver-version-sensitive, first split a large proof into smaller lemmas, remove irrelevant context, and make quantifier use more explicit. Increase `#[verifier::rlimit(...)]` only when the localized proof -still has a justified resource requirement. +still has a justified resource requirement. Keep the limit at or below `200`; +if a proof requires more, decompose or simplify it instead of raising the limit +further. An `rlimit` increase can be a temporary compatibility measure during a solver upgrade, but it should remain visible as proof debt and should not replace proof