[anneal] Add more thorough agent documentation#3489
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gaso4is5l3ore5u3xhbeclucymmqjxqz7 #3489 +/- ##
==================================================================
Coverage 91.85% 91.85%
==================================================================
Files 20 20
Lines 6093 6093
==================================================================
Hits 5597 5597
Misses 496 496 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
86af9d1 to
2b0a531
Compare
gherrit-pr-id: Gbzsorhgbclv3optfx2dkxjelijhcdfds
2b0a531 to
46856a9
Compare
| Read [the design principles](docs/design/principles.md) for the project's value | ||
| function and [the settled requirements](docs/design/settled-requirements.md) for |
There was a problem hiding this comment.
| Read [the design principles](docs/design/principles.md) for the project's value | |
| function and [the settled requirements](docs/design/settled-requirements.md) for | |
| Read [the design principles](docs/design/principles.md) for principles that guide all | |
| design decisions and | |
| [the settled requirements](docs/design/settled-requirements.md) for |
| 4. The [accepted-decision index](docs/design/decisions/README.md) and each | ||
| accepted decision relevant to the change. | ||
| 5. [Verification model](docs/design/verification-model.md), | ||
| [verification subject and result identity](docs/design/verification-artifact.md), and |
There was a problem hiding this comment.
The link text here doesn't make sense to me. Is there a different way of wording what is contained in the linked document?
| ## How to make judgment calls | ||
|
|
||
| Apply these rules together rather than as a rigid total ordering: | ||
|
|
||
| - Preserve soundness. Do not gain simplicity, coverage, or convenience by | ||
| weakening a soundness obligation or silently adding trust. | ||
| - Preserve semantic fidelity. A simple model is valuable only while it | ||
| faithfully supports the claim Anneal makes. Resource ownership, provenance, | ||
| initialization, concurrency protocols, or effects must not become freely | ||
| duplicable facts when doing so could invalidate soundness. | ||
| - Prefer local, compositional reasoning. The key scalability property is that | ||
| an implementation can be checked against an abstraction boundary and then | ||
| used without re-examining the whole program. | ||
| - Prefer the simplest faithful abstraction. Pure functional contracts are | ||
| excellent where they capture the interface; resource- or effect-aware | ||
| interfaces are required where purity would discard soundness-relevant facts. | ||
| - Make trust explicit and auditable. A trusted leaf can be a legitimate | ||
| engineering boundary; a hidden assumption or uncovered operation cannot. | ||
| - Build on maintained Lean, Aeneas, and Charon abstractions when they fit. | ||
| Reinvention is permitted, but should carry a concrete benefit that outweighs | ||
| duplicated semantics and maintenance. | ||
| - Prefer robust programmatic interfaces over textual patching. Upstream changes | ||
| to Aeneas, Charon, Lean libraries, and Rust itself are in scope. Choose | ||
| upstream or downstream ownership case by case, including the burden placed on | ||
| collaborators. | ||
| - Optimize for useful coverage, evolvability, debuggability, and eventual use | ||
| by ordinary Rust engineers. AI assistance is expected to help, but may not be | ||
| used to excuse an incoherent or unauditable interface. | ||
| - Support incremental adoption without confusing an assumption with a proof. | ||
| Prose safety justifications and incomplete proofs must remain visible in the | ||
| resulting trust or coverage report. | ||
| - Fail closed relative to the exact claim and command mode being reported. | ||
| Unsupported semantics, missing coverage, or an undischarged obligation may | ||
| never produce an unconditional verification claim. An explicitly named | ||
| incremental mode may report a weaker conditional result only when every | ||
| assumption and incomplete obligation is part of that result; command names | ||
| and exit policies remain open. | ||
|
|
||
| When principles conflict, state the conflict and justify the tradeoff in those | ||
| terms. Do not invent a permanent priority ordering from one local decision. |
There was a problem hiding this comment.
Should some or all of this live in the principles documentation instead?
| excellent where they capture the interface; resource- or effect-aware | ||
| interfaces are required where purity would discard soundness-relevant facts. | ||
| - Make trust explicit and auditable. A trusted leaf can be a legitimate | ||
| engineering boundary; a hidden assumption or uncovered operation cannot. |
There was a problem hiding this comment.
"uncovered" has a conventional meaning that is not what we intend; maybe more verbose is better? Something like "... or an operation that is ignored or not covered by proof reasoning logic"?
| Reinvention is permitted, but should carry a concrete benefit that outweighs | ||
| duplicated semantics and maintenance. |
There was a problem hiding this comment.
Should we specifically ask agents to flag abstractions that could be upstreamed to Lean, Aeneas, and/or Charon?
There was a problem hiding this comment.
Agreed. I'm not sure where best to put this guidance.
| - `docs/design/` states the normative intent. | ||
| - Accepted records in `docs/design/decisions/` capture settled choices and | ||
| their rationale. | ||
| - `docs/design/open-questions/` records constraints, candidates, and evidence, | ||
| not decisions. | ||
| - `docs/reference/` describes the checked-in implementation and may change as | ||
| the code changes. | ||
| - `docs/history/` is evidence, not authority. |
There was a problem hiding this comment.
Is this valuable if agents are going to go read the linked README.md that says as much anyway?
| project authors. With that agreement, add or update an accepted decision record | ||
| and reconcile the normative documents. Without it, keep the record proposed, | ||
| describe the implementation as an experiment, or stop and surface the choice. | ||
| If documents conflict, surface the conflict instead of silently selecting the |
There was a problem hiding this comment.
There is a technical notion of "conflict" that we don't want to mistakenly imply here. Maybe something like "the decisions in different documents" or "the proposals in different documents" or something?
| - the final property/outcome taxonomy; | ||
| - whether proof obligations are encoded as Lean arguments or sidecar theorems; | ||
| - how Anneal's property tracking builds on or parallels Rust's `unsafe` | ||
| machinery; | ||
| - the annotation and proof-authoring syntax; | ||
| - the precise boundary among Anneal, Aeneas, Charon, and rustc; | ||
| - the exact audit-ledger schema and success modes of `cargo anneal verify`. |
There was a problem hiding this comment.
This is likely to change. Should we "trust the content of docs/design/open-questions" (or whatever the path is) rather than put a one-off list here?
| ## Current implementation | ||
|
|
||
| The checked-in V2 executable currently provides toolchain setup scaffolding; | ||
| much of the intended verification pipeline is not yet present on this branch. | ||
| Open and stacked PRs may contain additional implementation, but are not the | ||
| source of truth for the checked-in tree. See | ||
| [current architecture](docs/reference/current-architecture.md). | ||
|
|
||
| From the repository root, useful checks are: | ||
|
|
||
| ```bash | ||
| cargo test --locked --manifest-path anneal/Cargo.toml | ||
| cargo fmt --check --manifest-path anneal/Cargo.toml --all | ||
| PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s anneal/tests -p 'test_*.py' | ||
| bash anneal/check-flake-eval.sh | ||
| ``` | ||
|
|
||
| Tests behind the `exocrate_tests` feature expect CI to place a prebuilt archive | ||
| at `anneal/target/anneal-exocrate.tar.zst`. | ||
|
|
||
| V1 has different commands and a different architecture. Follow | ||
| `anneal/v1/AGENTS.md` when working there. |
There was a problem hiding this comment.
I have observed that agents are pretty good t deducing "useful checks" (including adjustments needed to environment, features, etc. when documentation is wrong). Between that, and my bias against putting something in here that can bitrot or drift relative to more authoritative sources liek docs/design/**, I wonder whether we should omit this. If an agent needs to know the current state, they should look at git history, open issues, open PRs, and documents. I would suggest either omitting this section, or replacing it with a suggestion stating "how to find current state/conventions" instead of what they are.
There was a problem hiding this comment.
Recording a general observation discussed w/ @mdittmer: There is a lot of the current state of the repo encoded in this and other agent files that risks bit rotting or drifting. We should consider how much of that could be easily reconstructed by either reading the code directly or by reading documentation which lives "closer" to the code and is more likely to be kept up to date.
| outcomes carry which postconditions is part of the open property/outcome | ||
| design. | ||
|
|
||
| **Callee obligation** |
There was a problem hiding this comment.
Why is this not referred to as "caller obligation" given that it's an obligation placed on the caller?
| : The property that an implementation faithfully realizes its declared | ||
| interface in every client context covered by the claim. The coverage envelope | ||
| must be explicit: concrete calls in one compilation subject and a reusable | ||
| theorem quantified over downstream safe clients are different claims. Anneal | ||
| uses contextual refinement as the durable interpretation of the locality | ||
| behind safe encapsulation, rather than requiring literal syntactic | ||
| substitution of implementations. |
There was a problem hiding this comment.
This is pretty abstract. More plain language or examples might help clarify.
| The promise of safe Rust is that any type-checked use of a safe API from sound | ||
| safe code remains sound. An implementation using unsafe code can uphold this |
There was a problem hiding this comment.
| The promise of safe Rust is that any type-checked use of a safe API from sound | |
| safe code remains sound. An implementation using unsafe code can uphold this | |
| The promise of safe Rust is that any type-checked use of a safe API from | |
| safe code remains sound. An implementation using unsafe code can uphold this |
| - Lessons from V1 should be distilled into V2 history documents instead of | ||
| requiring contributors to reverse-engineer the prototype. | ||
|
|
||
| ## Alternatives considered |
There was a problem hiding this comment.
Delete this section - none of these were actually considered, and this fails to capture the reasoning. The reasoning isn't all that important now that we've made this decision anyway.
| # Anneal | ||
|
|
||
| Anneal is being built to help Rust developers prove that unsafe implementations | ||
| uphold the guarantees expected of safe Rust. |
There was a problem hiding this comment.
We don't need to hedge here; that's what the big status comment below is for.
| uphold the guarantees expected of safe Rust. | |
| Anneal helps Rust developers prove that unsafe implementations | |
| uphold the guarantees expected of safe Rust. |
Also, should we frame safety from unsafe code as a primary (and obligatory) use case for a general verification framework that embeds assertions and proofs in rust code?
| must uphold that safety promise even when it uses unsafe code internally. | ||
|
|
||
| Unsafe Rust lets a programmer perform operations that the compiler cannot | ||
| prove are valid. Each such operation comes with requirements: a pointer might |
There was a problem hiding this comment.
"valid" has a technical meaning in formal logic. Should we use "safe" instead?
|
|
||
| Because `get_byte` is a safe function, callers may pass any `usize`. An | ||
| out-of-bounds call may panic at the assertion, but it must never cause undefined | ||
| behavior. A safe API cannot place a hidden safety requirement on its caller. |
There was a problem hiding this comment.
"cannot" implies impossibility, which doesn't seem quite right. Perhaps "must not" is stronger than "should not", but does not imply impossibility?
| Anneal is intended to check reasoning like this instead of trusting the comment | ||
| alone. |
There was a problem hiding this comment.
Perhaps "automatically check" or "programmatically check" to imply how this is achieved?
|
|
||
| This is intentionally a tiny example; ordinary Rust should simply use | ||
| `bytes[index]`. It stands in for implementations which cannot avoid unsafe | ||
| operations. It contains no Anneal-specific syntax because's specification and |
There was a problem hiding this comment.
| operations. It contains no Anneal-specific syntax because's specification and | |
| operations. It contains no Anneal-specific syntax because specification and |
| could invalidate the claim. Resource tracking is an important example, not an | ||
| exhaustive list of cases requiring richer machinery. | ||
|
|
||
| In particular, a separation-logic resource must not become an unrestricted |
There was a problem hiding this comment.
Maybe "For example" instead of "In particular". A separation logic probably doesn't have special status among the various tools we might deploy to chip away at Aeneas's current caveats.
| At a high level, a function must establish its declared guarantees under its | ||
| preconditions and must meet the required preconditions or properties of every | ||
| callee. Property kinds may depend on one another. A soundness proof may, for | ||
| example, require a non-soundness property promised by another operation. |
There was a problem hiding this comment.
I do not understand the use of "non-soundness property" here. Is it a typo? Can we reword for greater clarity?
| rules for duplication, consumption, framing, opening, and re-establishment are | ||
| part of its meaning. | ||
|
|
||
| ## Compose obligations, not duplicated proofs |
There was a problem hiding this comment.
Maybe "Keep proofs DRY" or similar?
| specifications and `step`/`step*` tactics poorly. V2 is leaning toward shared, | ||
| combined reasoning, but the precise outcome and property architecture remains | ||
| open. The lesson is to avoid needless duplication, not to prematurely ratify a | ||
| replacement taxonomy. |
There was a problem hiding this comment.
I'm not sure we want to reify this example here. It's quite specific, and it's not yet clear how we want to achieve the desired effect. For example, keeping those two conditions separate may end up being a good strategy, but it should be coupled with auxiliary definitions or lemmas that can be reused in both proof contexts. Making it easy to structure things that way might end up being how this principle is realized, rather than abandoning the breakdown into two proof obligations.
| open. The lesson is to avoid needless duplication, not to prematurely ratify a | ||
| replacement taxonomy. | ||
|
|
||
| ## Prefer maintained foundations |
There was a problem hiding this comment.
Not to self: CONTINUE HERE. Reviewing things in more-or-less linked-from-AGENTS.md order.
3 participants
Latest Update: v3 — Compare vs v2
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gbzsorhgbclv3optfx2dkxjelijhcdfds && git checkout -b pr-Gbzsorhgbclv3optfx2dkxjelijhcdfds FETCH_HEADCheckout
git fetch origin refs/heads/Gbzsorhgbclv3optfx2dkxjelijhcdfds && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gbzsorhgbclv3optfx2dkxjelijhcdfds && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.