[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:
|
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.
46856a9 to
cbd157a
Compare
|
Addressed all comments and made other restructurings in this diff from v3 to v4 of this PR. |
|
|
||
| Rust compilers reserve the right to give arbitrary behavior to a program after | ||
| undefined behavior. Anneal's source models likewise promise correspondence | ||
| only while Rust's validity requirements hold. Soundness is therefore not just |
There was a problem hiding this comment.
| only while Rust's validity requirements hold. Soundness is therefore not just | |
| only when Rust program's behavior is defined. Soundness is therefore not just |
| checked against an abstraction boundary that every supported safe client may | ||
| then rely on. Clients should consume established interface guarantees rather |
There was a problem hiding this comment.
| checked against an abstraction boundary that every supported safe client may | |
| then rely on. Clients should consume established interface guarantees rather | |
| checked against an abstraction boundary that the implementer has proven sound. | |
| Clients should consume established interface guarantees rather |
| then rely on. Clients should consume established interface guarantees rather | ||
| than reopen private implementations or reason about an unrelated remainder of | ||
| the program. |
There was a problem hiding this comment.
I wonder whether we should have a stronger statement that refers to non-interference here (between a lexically scoped abstraction and the rest of the program).
| The durable formulation is contextual refinement: an implementation realizes | ||
| its declared interface in every supported context. The interface may include | ||
| values, effects, capabilities, resources, protocols, and invariants. Locality | ||
| does not require pretending that every implementation is a pure value | ||
| transformer. | ||
|
|
||
| Composition then has a uniform shape. Each item establishes its guarantees | ||
| under its assumptions, and each use establishes the requirements of the | ||
| operations it invokes. Property dependencies are evidence-graph edges. For | ||
| example, a callee's ordinary functional guarantee that an index is below a | ||
| buffer length may discharge the soundness requirement of a caller's raw | ||
| pointer access. | ||
|
|
There was a problem hiding this comment.
There's something about how this is written that fails to provide clarity for me. I think we should cut these two paragraphs and draft a brief statement about composition to wrap up the paragraph above.
| abstraction boundary. Preserve resource, provenance, initialization, | ||
| ownership, concurrency, protocol, and effect semantics whenever erasing them | ||
| could invalidate the claim. |
There was a problem hiding this comment.
Suggestion: replace "Preserve" with "Introduce" and "erasing" with "eliding" or "ignoring".
| account for the burden placed on collaborators. | ||
|
|
||
| ## Make trust explicit, classified, and reducible | ||
|
|
There was a problem hiding this comment.
We should explain "what trust means" to Anneal. I think we want something in the neighbourhood of "abstractions with semantics admitted without proof", but trust can mean different things in different contexts, even in security. A crisp statement of what we mean by trust will lend clarity to this subsection.
It may be that we need multiple notions of trust, too. What it means to trust a compiler or other tool might be different from trust the way tools composed, which might be different from trusting things spelled axiom in a Lean model. (The last of this is what I had in mind with my vague definition above.)
| evidence supports, and what would strengthen it. Favor stable proof interfaces, | ||
| diagnostics tied to Rust source, resilience to small program changes, and | ||
| failures that explain the outstanding obligation. |
There was a problem hiding this comment.
This is another example of "written as an agent instruction" inside documentation that should be approachable and pleasant for humans to read. (I admit there is some tension here between my request to "state an actual principle"--which will often sound directive--and "write documentation, not pithy agent instructions".) Maybe even "This principle favors" or similar would make this feel more like documentation that agent instructions.
| AI assistance may reduce the amount of formal expertise needed to author a | ||
| proof. It may not excuse an interface whose meaning or trust boundary Rust | ||
| engineers cannot audit. Performance and automation matter because feedback | ||
| latency shapes adoption, but neither may weaken or obscure the reported claim. | ||
|
|
There was a problem hiding this comment.
I think we should either drop this or give it its own principle.
In terms of style, this paragraph feels like its talking around what it means to say, rather than being straightforward.
I think the intent here is "don't let agents weasel their way out of required proof obligations". This aspiration feels like an implementation detail around syntax and tooling affordances that we are a long way from being able to address. I think the core principle here is mostly covered by "Make trust explicit, ...". It should be hard for humans or agents to "work around" any "hard obligations" that should be "difficult to erase". I see this as a consequence of "Make trust explicit, ...", but if we want to make it its own thing, I don't think it should be a paragraph under incremental adoption.
| ## Applying the principles | ||
|
|
||
| The principles often reinforce one another, but they do not define a permanent | ||
| total order. When they pull in different directions: | ||
|
|
||
| 1. state the exact claim each alternative would support; | ||
| 2. identify added trust, lost coverage, or erased semantic information; | ||
| 3. ask whether the result still composes at an abstraction boundary; | ||
| 4. consider usability, maintenance, and the path to broader coverage; | ||
| 5. prefer reversible experiments while evidence is weak; and | ||
| 6. record an irreversible choice explicitly. | ||
|
|
||
| A convenient design that compromises soundness or claim integrity is | ||
| unacceptable. Among designs that preserve those constraints, the balance of | ||
| simplicity, coverage, maintenance, and user experience is a case-specific | ||
| judgment. |
There was a problem hiding this comment.
I think humans engaged in human dialogue are going to decide together how to apply these principles. I would advocate for moving this to ### Instructions for agents applying these principles under ## Goals and scope.
| Rust execution to its Lean model. That gap must remain visible rather than | ||
| being hidden by successful Lean compilation. | ||
|
|
||
| ## Designs which should not be inherited |
There was a problem hiding this comment.
super-nit: Bold the word "not".
| the gap and identifies the operation which produced it instead of silently | ||
| treating the comment as proof. An undischarged obligation is a verification | ||
| failure and a useful diagnostic; by itself, it does not prove that the Rust | ||
| code is unsafe. |
There was a problem hiding this comment.
| code is unsafe. | |
| code is unsound. |
| code can still panic, run forever, or produce the wrong answer, but a safe API | ||
| must uphold that safety promise even when it uses unsafe code internally. | ||
|
|
||
| Unsafe Rust lets a programmer perform operations whose safety the compiler |
There was a problem hiding this comment.
| Unsafe Rust lets a programmer perform operations whose safety the compiler | |
| Unsafe Rust lets a programmer perform operations whose soundness the compiler |
cbd157a to
e35666f
Compare
gherrit-pr-id: Gbzsorhgbclv3optfx2dkxjelijhcdfds
e35666f to
9fe2da2
Compare
|
@mdittmer here's the diff based on our most recent feedback. |
3 participants
Latest Update: v7 — Compare vs v6
📚 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.