From 9fe2da2d6e1912258f3bfe77c713576737cbb4d4 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Fri, 17 Jul 2026 15:23:06 +0000 Subject: [PATCH] [anneal] Add more thorough agent documentation gherrit-pr-id: Gbzsorhgbclv3optfx2dkxjelijhcdfds --- anneal/AGENTS.md | 95 +++++ anneal/README.md | 169 ++++++++ anneal/agent_docs/README.md | 137 +++++++ anneal/agent_docs/agent-corpus.md | 93 +++++ .../design/decisions/0000-template.md | 57 +++ .../0001-v2-is-a-clean-room-redesign.md | 82 ++++ .../0002-verification-is-artifact-scoped.md | 94 +++++ .../0003-expanded-generated-rust-is-input.md | 96 +++++ ...4-invariants-support-all-property-kinds.md | 94 +++++ ...-adoption-supports-prose-justifications.md | 99 +++++ ...0006-the-tcb-is-explicit-and-shrinkable.md | 122 ++++++ anneal/agent_docs/design/decisions/README.md | 60 +++ .../design/open-questions/README.md | 76 ++++ .../aeneas-charon-integration.md | 151 +++++++ .../contracts-and-invariants.md | 176 +++++++++ .../memory-resources-and-effects.md | 159 ++++++++ .../proof-authoring-and-user-experience.md | 177 +++++++++ .../property-kinds-and-outcomes.md | 164 ++++++++ .../open-questions/rust-safety-integration.md | 165 ++++++++ .../open-questions/source-model-adequacy.md | 168 ++++++++ .../trust-and-incremental-adoption.md | 163 ++++++++ anneal/agent_docs/design/principles.md | 144 +++++++ anneal/agent_docs/design/result-and-trust.md | 374 ++++++++++++++++++ .../agent_docs/design/settled-requirements.md | 274 +++++++++++++ .../agent_docs/design/verification-model.md | 239 +++++++++++ anneal/agent_docs/design/worked-example.md | 226 +++++++++++ anneal/agent_docs/glossary.md | 247 ++++++++++++ anneal/agent_docs/history/research-index.md | 184 +++++++++ anneal/agent_docs/history/v1-lessons.md | 196 +++++++++ .../agent_docs/reference/aeneas-and-charon.md | 83 ++++ .../reference/current-priorities.md | 108 +++++ anneal/agent_docs/reference/current-state.md | 157 ++++++++ .../reference/development-and-ci.md | 146 +++++++ anneal/v1/AGENTS.md | 14 +- anneal/v1/README.md | 7 + 35 files changed, 4992 insertions(+), 4 deletions(-) create mode 100644 anneal/AGENTS.md create mode 100644 anneal/README.md create mode 100644 anneal/agent_docs/README.md create mode 100644 anneal/agent_docs/agent-corpus.md create mode 100644 anneal/agent_docs/design/decisions/0000-template.md create mode 100644 anneal/agent_docs/design/decisions/0001-v2-is-a-clean-room-redesign.md create mode 100644 anneal/agent_docs/design/decisions/0002-verification-is-artifact-scoped.md create mode 100644 anneal/agent_docs/design/decisions/0003-expanded-generated-rust-is-input.md create mode 100644 anneal/agent_docs/design/decisions/0004-invariants-support-all-property-kinds.md create mode 100644 anneal/agent_docs/design/decisions/0005-incremental-adoption-supports-prose-justifications.md create mode 100644 anneal/agent_docs/design/decisions/0006-the-tcb-is-explicit-and-shrinkable.md create mode 100644 anneal/agent_docs/design/decisions/README.md create mode 100644 anneal/agent_docs/design/open-questions/README.md create mode 100644 anneal/agent_docs/design/open-questions/aeneas-charon-integration.md create mode 100644 anneal/agent_docs/design/open-questions/contracts-and-invariants.md create mode 100644 anneal/agent_docs/design/open-questions/memory-resources-and-effects.md create mode 100644 anneal/agent_docs/design/open-questions/proof-authoring-and-user-experience.md create mode 100644 anneal/agent_docs/design/open-questions/property-kinds-and-outcomes.md create mode 100644 anneal/agent_docs/design/open-questions/rust-safety-integration.md create mode 100644 anneal/agent_docs/design/open-questions/source-model-adequacy.md create mode 100644 anneal/agent_docs/design/open-questions/trust-and-incremental-adoption.md create mode 100644 anneal/agent_docs/design/principles.md create mode 100644 anneal/agent_docs/design/result-and-trust.md create mode 100644 anneal/agent_docs/design/settled-requirements.md create mode 100644 anneal/agent_docs/design/verification-model.md create mode 100644 anneal/agent_docs/design/worked-example.md create mode 100644 anneal/agent_docs/glossary.md create mode 100644 anneal/agent_docs/history/research-index.md create mode 100644 anneal/agent_docs/history/v1-lessons.md create mode 100644 anneal/agent_docs/reference/aeneas-and-charon.md create mode 100644 anneal/agent_docs/reference/current-priorities.md create mode 100644 anneal/agent_docs/reference/current-state.md create mode 100644 anneal/agent_docs/reference/development-and-ci.md diff --git a/anneal/AGENTS.md b/anneal/AGENTS.md new file mode 100644 index 0000000000..8f11cd91d3 --- /dev/null +++ b/anneal/AGENTS.md @@ -0,0 +1,95 @@ + + +# Anneal agent guide + +This file governs work in `anneal/`. Work under `anneal/v1/` must also follow +the more specific `v1/AGENTS.md`. + +Anneal is a clean-room, ground-up redesign of the experimental V1 prototype. +V1 is useful evidence, not a default architecture, specification language, or +user interface. Reuse a V1 idea or implementation only after evaluating it +against the current design. + +## Mission + +Anneal is a general verification tool for Rust, with unsafe-code soundness as +its foundational use case. It aims to let ordinary Rust teams verify subtle +properties of real Rust programs while preserving the guarantees expected of +safe Rust. + +Soundness is non-negotiable. Rust compilers and Anneal's source models need not +preserve a program's behavior after undefined behavior, so Anneal must establish +the soundness conditions on which its own model fidelity depends. Never gain +simplicity, coverage, or convenience by weakening such a condition, silently +omitting an operation, or hiding trust. + +## Start here + +`agent_docs/` is the canonical project context and design corpus written for +coding agents. It is not Anneal's user-facing documentation surface. Human +maintainers may read and edit it, but its organization and wording should be +optimized for agent ingestion and judgment. + +In an unfamiliar checkout, first complete the +[agent-corpus preflight](agent_docs/agent-corpus.md). Then follow the canonical +[documentation map](agent_docs/README.md), which owns the reading order, +document authority, and reconciliation procedure for the design canon. + +## Working protocol + +- Evaluate alternatives using the + [design principles](agent_docs/design/principles.md) and satisfy every + applicable + [settled requirement](agent_docs/design/settled-requirements.md). +- Follow accepted decision records. Treat open-question documents, issues, + pull requests, research, experiments, and V1 as evidence rather than settled + authority. +- Do not settle an open design incidentally in implementation. Before a change + commits the project to an answer, obtain explicit agreement from the project + authors and record the accepted decision. Otherwise label the implementation + as an experiment or surface the choice. +- If documents disagree, surface and reconcile the disagreement using the + process in the documentation map instead of silently choosing convenient + text. +- Fail closed relative to the exact claim being reported. Unsupported + semantics, omitted coverage, hidden assumptions, and undischarged obligations + must not produce an unconditional verification claim. +- Determine current behavior from the checked-in code and the + [current-state reference](agent_docs/reference/current-state.md). Open or + stacked pull requests may provide context, but are not authoritative for the + current checkout. +- Prefer existing, maintained Lean, Aeneas, Charon, and Rust mechanisms when + they fit. Flag abstractions or extensions which may belong upstream; decide + ownership case by case, including the maintenance burden on collaborators. +- Prefer robust programmatic interfaces over textual patching and keep the + proof and diagnostic experience usable by ordinary Rust engineers. + +### Applying the design principles + +When settled requirements and accepted decisions do not determine an answer: + +1. state the exact claim each alternative would support; +2. identify added trust, lost coverage, or omitted semantic information; +3. ask whether the result still composes at an established abstraction + boundary; +4. consider usability, maintenance, and the path to broader coverage; +5. prefer reversible experiments while evidence is weak. + +## Documentation maintenance + +- Update the design canon in the same change that alters a settled contract, + trust boundary, or project-wide constraint. +- Give requirements stable identifiers and link implementation decisions back + to them. +- Record meaningful evidence and rejected alternatives, but remove temporary + misunderstandings once terminology has been clarified. +- Keep current-state references synchronized with checked-in behavior. Issues + and pull requests are guides to thinking, not specifications. +- Link to each explanation's canonical owner instead of duplicating it across + agent instructions or corpus pages. diff --git a/anneal/README.md b/anneal/README.md new file mode 100644 index 0000000000..f9df49bc9b --- /dev/null +++ b/anneal/README.md @@ -0,0 +1,169 @@ + + +# Anneal + +Anneal is a verification tool for Rust. It helps developers replace informal +reasoning about unsafe code with checked proofs, and it can also verify precise +application-specific promises about program behavior. + +> **Status:** Anneal is under active construction and cannot yet verify +> applications. The checked-in executable currently provides only toolchain +> setup infrastructure. The example below illustrates the problem Anneal +> addresses, not a workflow which is currently available. + +## Why Anneal exists + +Rust's safe APIs promise that ordinary, type-checked use will not cause +undefined behavior—for example, an invalid memory access or a data race. We +call this guarantee soundness: every use which the safe API permits must remain +free from undefined behavior. Safe code can still panic, run forever, or +produce the wrong answer, but a safe API must remain sound even when it uses +unsafe code internally. + +Unsafe Rust lets a programmer perform operations whose soundness the compiler +cannot verify. Each such operation comes with requirements: a pointer might +need to refer to live memory, an index might need to be in bounds, or a value +might need to be initialized. The compiler accepts the operation because the +programmer takes responsibility for meeting those requirements. + +That reasoning is usually recorded in a comment: + +```rust +pub fn get_byte(bytes: &[u8], index: usize) -> u8 { + assert!(index < bytes.len()); + + // SAFETY: `bytes` is a valid slice and `index` is in bounds, so this + // pointer may be dereferenced. + unsafe { *bytes.as_ptr().add(index) } +} +``` + +A reviewer can understand this argument, but Rust does not check that the +comment is correct or remains correct after a refactor. If the bounds check is +removed or moved too late, the unsafe operation's requirements may no longer +hold while the comment continues to look reassuring. + +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 must not place a hidden safety requirement on its caller. + +Anneal turns reasoning like the safety comment into proof obligations checked +by [Lean](https://lean-lang.org/), a language which mechanically checks +mathematical arguments. If Anneal cannot establish an obligation, it reports +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 unsound. + +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 the specification +and proof-authoring interface is still being designed. + +## What Anneal adds + +Anneal lets a project describe: + +- the requirements a caller must satisfy before using an unsafe API; +- the promises a function or type makes to its callers; and +- the reasoning which connects ordinary Rust code to those requirements and + promises. + +Anneal checks the Rust safety obligations within the claimed scope, including +the requirements of unsafe operations and the promises on which safe APIs +rely. It follows those promises through function calls, so a verified +implementation can be used through its API without every caller re-examining +its private unsafe code. + +For a safe abstraction, the goal is straightforward: callers can use the safe +API according to the normal Rust type system, with no hidden rule whose +violation could cause undefined behavior. An unsafe API may explicitly give +part of that responsibility to its caller—for example, through a function +declared `unsafe` with documented requirements. + +## What a verification result means + +**Note:** The exact report format and command behavior are still being designed. + +A successful Anneal result identifies the particular code and build it covers +and states which guarantees were checked. At a minimum, it establishes that: + +- every safety-relevant operation within the named coverage satisfies Rust's + requirements; +- the functions and types checked by Anneal keep the promises stated in their + specifications; and +- anything Anneal could not prove, deliberately trusted, or did not cover is + listed rather than silently included in an unconditional claim. + +For example, a result might cover one Cargo target with a particular feature +set and dependency graph. It should say whether generated Rust, dependencies, +and calls into foreign code were checked, trusted, or outside its coverage. + +When Anneal reports that a safe abstraction itself has been verified within a +stated semantic and build envelope, every type-correct safe use which the API +permits within that envelope should be safe—not only the calls which happened +to appear in one test or binary. Any assumptions on that claim must be listed +explicitly. + +Verification does not mean that the program has no bugs. It applies only to +the guarantees and build configuration named in the result. Changing the +target, feature set, dependency, compiler configuration, or generated source +may require checking the program again. + +For promises beyond Rust safety, Anneal checks whether the code satisfies the +specification it was given; it cannot decide whether that specification says +what its author truly wanted. A weak or mistaken specification can describe +the wrong behavior. It cannot, however, erase the Rust safety requirements +which Anneal is responsible for checking. + +## Beyond Rust safety + +Rust safety is only one part of program correctness. A memory-safe function can +still return the wrong answer or panic unexpectedly. Anneal also aims to check +additional promises, for example: + +- a parser returns the value described by its input; +- an operation does not panic when its documented requirements hold; +- a data structure preserves the rules expected by its public API; or +- an implementation follows an application or network protocol. + +Each promise must be stated precisely enough to prove. Anneal should make +common cases approachable while leaving Lean available for specifications and +proofs which need its full expressive power. + +## Incremental adoption + +Adopting formal verification across an existing codebase takes time. Anneal +lets teams begin with their highest-risk code and expand coverage gradually. + +During that process, some unsafe operations may still rely on prose +`// SAFETY:` comments, unfinished proofs, or trusted external behavior. Anneal +reports those portions honestly rather than treating them as machine-checked +facts. This lets a team see what has been proved and what work or trust remains. + +## Under the hood: Lean + +Lean checks Anneal's mathematical arguments. Some specifications or advanced +proofs may be written directly in Lean, while Anneal connects them to the Rust +program and presents useful obligations and diagnostics to Rust developers. + +Lean can check only the statement it receives. A meaningful result therefore +also depends on Anneal connecting that statement to the right Rust program and +reporting any external assumptions. Users should not need to understand the +translation machinery, but they must be able to see the assumptions and gaps +which qualify a result. + +## Repository development + +Coding agents working on Anneal must begin with [`AGENTS.md`](AGENTS.md). It +routes them into `agent_docs/`, an internal corpus written for agent +consumption. That corpus contains design context, current implementation facts, +and operating guidance which are intentionally omitted from this user-facing +introduction. Human maintainers may consult it, but it is not part of Anneal's +user documentation or a stable product interface. diff --git a/anneal/agent_docs/README.md b/anneal/agent_docs/README.md new file mode 100644 index 0000000000..2adce26398 --- /dev/null +++ b/anneal/agent_docs/README.md @@ -0,0 +1,137 @@ + + +# Anneal agent documentation + +This directory is the canonical project context and design corpus written for +coding agents working on the current Anneal redesign. It is not user-facing +documentation or a stable product interface. Human maintainers may inspect, +review, and edit it, but its structure and explanations should optimize agent +comprehension, judgment, and reliable action. + +Agent-oriented organization does not mean prompt-fragment prose. Design pages +should explain rationale declaratively in language human maintainers can audit; +imperative agent procedure belongs in `AGENTS.md` or an explicitly labeled +instruction section. + +This page is the canonical owner of the agent reading order, document +authority, and reconciliation process. Other agent instructions may point here, +but must not maintain a competing copy of that information. + +## Reading order + +Agents should first follow [`AGENTS.md`](../AGENTS.md). In an unfamiliar +checkout, complete the [agent-corpus preflight](agent-corpus.md) before relying +on any local document. + +Before making or reviewing a design change, read the following completely, in +order: + +1. The user-facing [project introduction](../README.md), to understand the + audience and product promise. +2. [Glossary](glossary.md), for stable vocabulary used throughout the canon. +3. [Principles](design/principles.md), for the goals and choice rules behind + design judgment. +4. [Settled requirements](design/settled-requirements.md), for constraints + every acceptable design must meet. +5. [Accepted decisions](design/decisions/README.md), including every decision + relevant to the change. +6. [Verification model](design/verification-model.md), for the intended local + proof and global composition argument. +7. [Result and trust model](design/result-and-trust.md), for the identity and + scope of a claim, its evidence, its residual dependencies, and what must be + reported. +8. [Worked example](design/worked-example.md), as an illustration whose + concrete proof choices are not decisions unless the text cites one. +9. [Open questions](design/open-questions/README.md), including every page + relevant to the task. Candidate approaches are not decisions. +10. [Current state](reference/current-state.md) and the explicitly + non-normative [current priorities](reference/current-priorities.md), for + checked-in behavior and the present engineering frontier. + +For translation, semantics, or proof-infrastructure work, also read +[Aeneas and Charon](reference/aeneas-and-charon.md). Read +[development and CI](reference/development-and-ci.md) before changing commands +or automation. Read [V1 lessons](history/v1-lessons.md) before borrowing from +the prototype, and inspect V1 itself only when the task requires primary +historical evidence. + +The [agent-corpus guide](agent-corpus.md) explains how to discover every +documentation file for a full audit or context-free comprehension test. + +## Document classes + +### Navigation and vocabulary + +This map, the [agent-corpus guide](agent-corpus.md), and the +[glossary](glossary.md) help readers find and interpret the canon. They do not +create design commitments independently of the normative documents and +accepted decisions they describe. + +### Normative design + +The files directly under [`design/`](design/) give the current consolidated +design. Principles guide choices; settled requirements constrain every +acceptable design. The worked example is a teaching companion: its concrete +choices are illustrative, and only the requirements and decisions it cites are +normative. + +### Accepted decisions + +Records under [`design/decisions/`](design/decisions/README.md) capture an +accepted choice, its rationale, and its consequences. A decision changes only +through an explicit amendment or superseding record. Consolidated design files +must be updated when such a change affects their account. + +### Open questions + +Files under [`design/open-questions/`](design/open-questions/README.md) are +design workspaces. Their settled constraints come from the normative documents +and accepted decisions they cite. Candidate approaches, provisional analyses, +and implementation experiments do not settle the question. + +### Reference + +Files under [`reference/`](reference/current-state.md) describe checked-in +code, commands, external tools, and current limitations. They are factual, not +aspirational. The dated +[current-priorities page](reference/current-priorities.md) is non-normative +guidance for the present engineering frontier. References must label intended +future roles and defer to the normative design where appropriate. + +### History and research + +Files under [`history/`](history/v1-lessons.md) preserve evidence, lessons, and +source indexes. V1, issues, pull requests, and research papers may motivate a +decision but do not override the current canon. Volatile source indexes must be +dated. + +## Resolving disagreements + +If normative files disagree with one another, or a consolidated design file +disagrees with an accepted decision, do not silently select one. Check whether +one record explicitly supersedes the other, then surface and repair the +inconsistency. Until it is reconciled, avoid making an irreversible design +choice which depends on the disputed point. + +Do not promote language from an open question, issue, pull request, experiment, +or V1 into a settled claim merely because it is convenient or has been +implemented. Record the decision first or continue to label the implementation +as an experiment. + +## Changing the canon + +A project-wide question becomes settled only with explicit agreement from the +project authors; implementation alone is not ratification. After agreement: + +1. add or update an accepted decision record; +2. update the relevant normative design files; +3. update the status and links of affected open questions; +4. update current-state references if checked-in behavior changed; and +5. preserve significant evidence and genuinely considered alternatives without + retaining obsolete conversational misunderstandings. diff --git a/anneal/agent_docs/agent-corpus.md b/anneal/agent_docs/agent-corpus.md new file mode 100644 index 0000000000..fbe5ebd73f --- /dev/null +++ b/anneal/agent_docs/agent-corpus.md @@ -0,0 +1,93 @@ + + +# Anneal agent corpus + +This page helps a context-free agent find and ingest the current Anneal agent +documentation without confusing a worktree container, another checkout, or +the historical V1 prototype for the intended corpus. The +[documentation map](README.md) is the sole owner of reading order and document +authority. + +## Establish the Anneal root + +Resolve the repository root from the current checkout; never copy an absolute +path from another session. The corpus root is its `anneal/` directory, which +must contain the crate and the documentation entrypoints: + +```bash +repo_root="$(git rev-parse --show-toplevel)" +anneal_root="$repo_root/anneal" + +test -f "$anneal_root/Cargo.toml" +test -f "$anneal_root/AGENTS.md" +test -f "$anneal_root/README.md" +test -f "$anneal_root/agent_docs/README.md" +test -f "$anneal_root/agent_docs/agent-corpus.md" +``` + +These structural checks deliberately avoid exact headings, hashes, and byte +counts. Routine documentation edits should not break discovery. If a marker is +missing, stop and locate the correct worktree instead of substituting a +similarly named directory. + +## Exclude V1 + +`anneal/v1/` is the historical prototype and is **not part of the current +corpus**. Do not recursively ingest it, follow its `AGENTS.md` as current +instructions, or use its README to replace a missing current file. Read +selected V1 documentation or source only when current documentation calls for +historical evidence, and treat it as history rather than authority. The +[V1 lessons](history/v1-lessons.md) page is the normal starting point. + +An `AGENTS.md` above `anneal/` may still impose repository or worktree +procedures. Those instructions apply to repository operations, but do not +replace Anneal's project and design canon. + +## Discover the complete corpus + +For a full documentation audit or a context-free comprehension test, read: + +- `anneal/AGENTS.md`; +- `anneal/README.md`; and +- every Markdown file under `anneal/agent_docs/`, recursively. + +Discover the last category from the filesystem instead of maintaining another +hand-written enumeration: + +```bash +find "$anneal_root/agent_docs" -type f -name '*.md' \ + ! -path '*/design/decisions/0000-template.md' -print | sort +``` + +Follow the order in the [documentation map](README.md). Do not add +`anneal/v1/**/*.md` to the corpus. Source code, issues, pull requests, and +upstream documentation may be necessary evidence for a task, but reading them +alongside the corpus does not give them design authority. + +`design/decisions/0000-template.md` is authoring scaffolding rather than a +decision, so it is deliberately excluded from a comprehension corpus. + +## Completion check + +After reading, a context-free agent should be able to explain, without relying +on V1 or an open pull request: + +- Anneal's product goal, intended users, and why soundness is foundational; +- the principles used to compare designs and the constraints every acceptable + design must satisfy; +- which documents are normative, accepted, open, factual, or historical; +- how an identified Rust subject, a precise claim, checked evidence, and + classified residual dependencies form a reported result; +- how local proofs compose into a global claim and why the source model must be + adequate for that argument; +- what the checked-in executable actually implements today; and +- which unresolved choice the current task must not settle silently. + +If the corpus does not support one of those answers, report the gap rather than +importing an answer from V1, an issue, or a pull request. diff --git a/anneal/agent_docs/design/decisions/0000-template.md b/anneal/agent_docs/design/decisions/0000-template.md new file mode 100644 index 0000000000..655302d089 --- /dev/null +++ b/anneal/agent_docs/design/decisions/0000-template.md @@ -0,0 +1,57 @@ + + +# NNNN: Short decision title + +- **Status:** Proposed +- **Date:** YYYY-MM-DD + +## Context + +Describe the problem, the constraints already settled elsewhere, and why a +decision is needed. Separate observations from assumptions. + +## Decision + +State the decision precisely enough that an implementer can tell whether a +proposal complies with it. Prefer a narrow commitment over settling adjacent +questions without evidence. + +## Rationale + +Explain how this decision follows from Anneal's [principles](../principles.md) +and why the tradeoff is appropriate. + +## Consequences + +List the useful constraints and the costs this decision introduces. Include +effects on soundness, user-visible claims, maintainability, and migration when +they are relevant. + +## Alternatives considered + +Describe credible alternatives and why they were not chosen. Not choosing an +alternative now need not mean rejecting it forever. + +## Deferred questions + +List choices this record intentionally does not make. Link them to the relevant +[open-question document](../open-questions/README.md) where possible. + +## Evidence + +Link primary sources, experiments, V1 lessons, or explicit design conclusions +which support the decision. Mark historical or potentially stale sources as +such. + +## Links + +- [Design principles](../principles.md) +- [Settled requirements](../settled-requirements.md) +- Related decisions and open questions + diff --git a/anneal/agent_docs/design/decisions/0001-v2-is-a-clean-room-redesign.md b/anneal/agent_docs/design/decisions/0001-v2-is-a-clean-room-redesign.md new file mode 100644 index 0000000000..645a94dc10 --- /dev/null +++ b/anneal/agent_docs/design/decisions/0001-v2-is-a-clean-room-redesign.md @@ -0,0 +1,82 @@ + + +# 0001: V2 is a clean-room redesign + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +Anneal V1 was an early experiment and demonstration. It established that parts +of the idea were useful, but it also embedded provisional choices about syntax, +proof structure, trust, and integration with Aeneas. Treating those choices as +an inherited compatibility surface would turn experiments into constraints +before V2's requirements are understood. + +V1 remains valuable evidence. Some of its code and designs may still be the +best way to implement a V2 requirement. + +## Decision + +Anneal V2 is a clean-room, ground-up rewrite and redesign. The presence of a +concept, interface, or implementation in V1 creates no presumption that V2 will +retain it. + +V2 may borrow or copy from V1 when a fresh evaluation shows that doing so serves +V2's principles and requirements. V2 documentation may refer to V1 to record a +lesson, or after a V1 choice has independently been accepted for V2. In all +other cases, V1 is historical context rather than design authority. + +Here, “clean-room” describes design inheritance; it is not a prohibition on +reusing suitable code. + +## Rationale + +Anneal's purpose requires substantial changes to the prototype. Starting from +the desired assurance and user experience keeps accidental V1 constraints from +outweighing soundness, semantic fidelity, composability, or maintainability. +Retaining V1 as evidence still lets V2 benefit from working code and hard-won +lessons. + +## Consequences + +- V2 proposals must be justified from current requirements and principles, not + merely by matching V1. +- Compatibility with V1 syntax, generated Lean, or workflows is not a default + requirement. +- Copying a V1 component requires checking that its assumptions still hold. +- V1 documentation lives under [`v1/`](../../../v1/) and must not be read as V2 + documentation. +- Lessons from V1 should be distilled into V2 history documents instead of + requiring contributors to reverse-engineer the prototype. + +## Deferred questions + +- Which V1 components, if any, should be reused? +- Will V2 offer migration tools or compatibility syntax for V1 users? +- What specification language, proof surface, and generated-Lean interface + should V2 expose? + +Those questions belong in the relevant +[open design discussions](../open-questions/README.md), not in this record. + +## Evidence + +- The project author explicitly characterized V1 as an early experimental and + demonstration prototype and V2 as a clean-room redesign. +- The [V1 design document](../../../v1/docs/design/design.md) records several + prototype-specific choices which are being reconsidered. +- [V1 lessons](../../history/v1-lessons.md) distills the evidence that should + inform V2 without becoming implicit precedent. + +## Links + +- [Design principles](../principles.md) +- [Settled requirements](../settled-requirements.md) +- [V1 lessons](../../history/v1-lessons.md) diff --git a/anneal/agent_docs/design/decisions/0002-verification-is-artifact-scoped.md b/anneal/agent_docs/design/decisions/0002-verification-is-artifact-scoped.md new file mode 100644 index 0000000000..1c8b02ffff --- /dev/null +++ b/anneal/agent_docs/design/decisions/0002-verification-is-artifact-scoped.md @@ -0,0 +1,94 @@ + + +# 0002: Verification is artifact-scoped + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +The meaning of Rust source depends on its compilation. Target, enabled features, +`cfg` values, panic strategy, dependency resolution, compiler behavior, and +environmental inputs can all change the program which is compiled. A claim +phrased only as “this library is verified” would therefore leave its subject +ambiguous. + +Anneal may eventually help users verify a matrix of configurations, but a +matrix is a collection of claims and not the initial atomic claim. + +## Decision + +The initial unit of an Anneal source-level verification claim is one Cargo +compilation artifact under a fixed target, configuration, feature set, panic +strategy, dependency graph, and relevant environment. + +A successful verification of one artifact does not imply that another target +or configuration has been verified. A command may eventually orchestrate +several artifacts, but each artifact remains a separately identified claim. + +## Rationale + +Scoping the claim to the program the compiler actually constructs makes it +precise and auditable. It avoids universal claims over code configurations that +Anneal has not analyzed while leaving room for higher-level matrix tooling. + +## Consequences + +- Verification output must identify its compilation subject sufficiently for a + user or auditor to distinguish it from other builds. +- Changing a claim-relevant compilation input produces a different artifact and + requires a new verification claim. +- Cross-target or all-features assurance requires verifying every intended + artifact or separately proving why the claim generalizes. +- Caches must not reuse a result across claim-relevant inputs without a sound + equivalence argument. +- The exact compilation-subject identity, verification-result identity, and + audit-ledger schema remain design work. + +## Alternatives considered + +### Claim verification for the source tree + +A source tree admits many semantically different builds, so this would obscure +which program was analyzed. + +### Require an entire configuration matrix as the atomic unit + +This would make early adoption unnecessarily expensive and still require a +definition of which matrix is complete. + +### Scope only to a crate and target triple + +Features, `cfg`, dependencies, panic behavior, and environmental inputs can +change semantics even when those two values are unchanged. + +## Deferred questions + +- Which inputs must be recorded, normalized, or content-addressed? +- Which host tools, environment variables, compiler flags, and target + specifications can change the compilation subject, and which instead belong + only to verification-result identity or the trust ledger? +- Should `cargo anneal verify` support build matrices, and how should it report + aggregate results? +- How do compilation-subject and verification-result identities appear in the + TCB audit ledger? + +## Evidence + +- The project author selected one fixed Cargo compilation artifact, rather than + a matrix of builds, as the exact initial unit of a source-level claim. +- Rust's compilation model makes target, `cfg`, features, panic strategy, + dependencies, and generated inputs semantically relevant. + +## Links + +- [Generated Rust is input](0003-expanded-generated-rust-is-input.md) +- [The TCB is explicit and shrinkable](0006-the-tcb-is-explicit-and-shrinkable.md) +- [Trust and incremental adoption](../open-questions/trust-and-incremental-adoption.md) +- [Design principles](../principles.md) diff --git a/anneal/agent_docs/design/decisions/0003-expanded-generated-rust-is-input.md b/anneal/agent_docs/design/decisions/0003-expanded-generated-rust-is-input.md new file mode 100644 index 0000000000..c8beccc0ed --- /dev/null +++ b/anneal/agent_docs/design/decisions/0003-expanded-generated-rust-is-input.md @@ -0,0 +1,96 @@ + + +# 0003: Expanded, generated Rust is verification input + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +Procedural macros and build scripts can generate Rust which becomes part of the +compiled program. Trusting a generator in place of analyzing its output would +exclude real program behavior from Anneal's claim. Requiring generated Rust to +be checked in would also misrepresent normal Cargo builds. + +This decision concerns generated Rust that enters the program seen by Charon. +It does not by itself settle how to treat every side effect of a build script, +foreign libraries selected for linking, or generator execution as a separate +program. + +## Decision + +Rust generated by procedural macros or build scripts and subsequently ingested +by Charon is verification input, just like checked-in Rust source. Its origin +does not exempt it from the obligations that apply to the rest of the compiled +artifact. + +The generator is not trusted as a substitute for checking the generated Rust. +Anneal analyzes the expanded program which participates in the artifact's +semantics. + +## Rationale + +Anneal's claim must track the code which is compiled, not only the files a human +checked into version control. Treating expanded code uniformly improves +semantic fidelity and lets ordinary Rust projects use their existing code +generation practices without adding generated source to the repository. + +## Consequences + +- Anneal must obtain an authoritative representation of generated Rust from the + compiler pipeline. +- Generated code can introduce proof obligations and trusted leaves just as + handwritten code can. +- Diagnostics should retain useful provenance back to a macro invocation or + generator where the toolchain makes that possible. +- The compilation-subject identity must account for inputs that can change + generated code. +- This record does not choose LLBC-only ingestion, a compiler metadata service, + or a source-level annotation scanner. + +## Alternatives considered + +### Trust procedural macros and build scripts + +That would place arbitrary generated program behavior outside the checked +artifact and unnecessarily enlarge the TCB. + +### Analyze only checked-in source + +The analyzed program could then differ from the program rustc compiles. + +### Require generated Rust to be checked in + +This does not match common Rust workflows and would not prove that the checked- +in output is the output used for the verified compilation. + +## Deferred questions + +- Which Charon or rustc interface should expose expanded code, annotations, item + identities, and call metadata? +- How should diagnostics map generated definitions to their source origins? +- Which build-script effects change the compilation subject, and which belong + only to verification-result identity or the trust ledger? +- How should generated native code, linked libraries, and other non-Rust output + be modeled? +- Must generator execution itself be reproducible or verified? + +## Evidence + +- The project author explicitly classified proc-macro- and build-script- + generated Rust as input which Charon ingests, rather than trusted source. +- Charon's compiler-derived program representation already includes code after + Rust compilation has resolved forms that a source-only scanner cannot fully + recover. + +## Links + +- [Verification is artifact-scoped](0002-verification-is-artifact-scoped.md) +- [Aeneas and Charon integration](../open-questions/aeneas-charon-integration.md) +- [Source/model adequacy](../open-questions/source-model-adequacy.md) diff --git a/anneal/agent_docs/design/decisions/0004-invariants-support-all-property-kinds.md b/anneal/agent_docs/design/decisions/0004-invariants-support-all-property-kinds.md new file mode 100644 index 0000000000..487dbad048 --- /dev/null +++ b/anneal/agent_docs/design/decisions/0004-invariants-support-all-property-kinds.md @@ -0,0 +1,94 @@ + + +# 0004: Invariants support all property kinds + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +V1 explored type invariants under the name `isValid` and trait invariants under +the name `isSafe`. Those names suggest that one mechanism concerns validity and +the other concerns soundness. V2 must support soundness, but users also need +invariants for other properties: panic freedom, protocol correctness, +cryptographic conditions, resource bounds, and domains not designed yet. + +The exact taxonomy and notation for property kinds remain open. + +## Decision + +Both type invariants and trait invariants must support arbitrary property kinds. +Neither mechanism is intrinsically restricted to soundness or to one built-in +notion of safety. + +Soundness remains special and non-negotiable. Generalizing invariant mechanisms +does not permit another selected property to weaken, replace, or bypass the +obligations required for sound Rust. + +## Rationale + +Types and trait bounds are important abstraction boundaries regardless of the +property being composed. A common architecture avoids duplicating an invariant +system for every domain and leaves V2 extensible to properties whose proof +backends arrive later. Preserving soundness as a mandatory foundation keeps +extensibility from weakening the primary assurance. + +## Consequences + +- V2's invariant representation cannot hard-code type invariants as “validity” + or trait invariants as “soundness.” +- Implementations and consumers need a way to identify which property an + invariant establishes or assumes. +- Adding a new property domain must not require replacing the type- or trait- + invariant architecture. +- Initial V2 need not implement specialized proof backends for every possible + property kind; the architecture must leave room for them. +- The V1 names and enforcement mechanisms are not accepted by this decision. + +## Alternatives considered + +### Restrict both invariant forms to soundness + +This would require parallel mechanisms to express the same abstraction pattern +for other correctness properties. + +### Reserve type invariants for validity and trait invariants for soundness + +The distinction follows V1 terminology rather than a fundamental difference in +where property-carrying invariants are useful. + +### Defer extensibility until another property backend exists + +That risks embedding soundness-specific assumptions in interfaces which are +difficult to generalize later. + +## Deferred questions + +- What are property kinds called and how are they declared or selected? +- How are type invariants established, invalidated, opened, and re-established? +- How are trait invariants enforced at implementation sites and made available + through a bound? +- How does Anneal integrate invariant access with Rust's existing `unsafe` + machinery or an Anneal-specific parallel analysis? +- How are dependencies and cycles between property kinds represented? +- What should replace the V1 `isValid` and `isSafe` syntax? + +## Evidence + +- The project author explicitly required both type invariants and trait + invariants to support arbitrary property kinds. +- Experience with V1 showed that its names and partial enforcement did not + express this general architecture; see [V1 lessons](../../history/v1-lessons.md). + +## Links + +- [Contracts and invariants](../open-questions/contracts-and-invariants.md) +- [Property kinds and outcomes](../open-questions/property-kinds-and-outcomes.md) +- [Rust safety integration](../open-questions/rust-safety-integration.md) +- [Design principles](../principles.md) diff --git a/anneal/agent_docs/design/decisions/0005-incremental-adoption-supports-prose-justifications.md b/anneal/agent_docs/design/decisions/0005-incremental-adoption-supports-prose-justifications.md new file mode 100644 index 0000000000..ffe9df39c3 --- /dev/null +++ b/anneal/agent_docs/design/decisions/0005-incremental-adoption-supports-prose-justifications.md @@ -0,0 +1,99 @@ + + +# 0005: Incremental adoption supports prose justifications + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +Real Rust codebases already justify unsafe operations with prose such as +`// SAFETY:` comments. Requiring every relevant obligation to be formalized and +proved before Anneal provides any value would make adoption all-or-nothing. +Conversely, silently treating prose as a machine proof would make Anneal's +assurance misleading. + +The relationship between Anneal property tracking and Rust's existing `unsafe` +machinery remains an open design question, but incremental adoption is a +requirement under either architecture. + +## Decision + +Anneal must support an incremental-adoption mechanism in which selected formal +proof obligations may temporarily be represented by prose safety +justifications. + +Every such substitution is an explicit, auditable trust assumption. Anneal +must not report or consume it as if it were a completed machine-checked proof, +and a user must be able to discover it when evaluating the resulting assurance. + +This record requires the capability; it does not decide its syntax, which +obligations may use it, or the success semantics of a command that encounters +one. + +## Rationale + +Incremental adoption lets users formalize high-value portions of an existing +codebase without first rewriting every safety comment. Making the remaining +human reasoning explicit preserves honest claims and provides a measurable path +toward a fully formal result. + +## Consequences + +- Anneal needs a durable association between a prose justification and the + obligation it stands in for. +- Trust reports must expose which obligations rely on prose rather than a + completed proof; how the final ledger categorizes those assumptions remains + open. +- Results containing prose justifications are conditional on their correctness. +- Tooling should make it possible to find and reduce the remaining prose + obligations over time. +- Integration with familiar Rust comments is possible but not mandated by this + record. + +## Alternatives considered + +### Require complete formalization before running Anneal + +This gives a simple final state but does not support the required path for +adopting Anneal in an existing codebase. + +### Treat every unproved obligation as an unrestricted axiom + +This loses the connection to the relevant Rust operation and obscures the +different reasons that facts remain trusted. + +### Silently skip obligations without proofs + +That would make success impossible to interpret and would violate the need for +an auditable trust boundary. + +## Deferred questions + +- What syntax associates prose with an Anneal obligation? +- Which obligations may use prose and under which command or policy? +- Does a result with prose assumptions exit successfully as “conditionally + checked,” or use another status distinct from “verified”? +- How are review, ownership, expiry, and migration of prose assumptions tracked? +- How should this mechanism build on Rust `unsafe` blocks, safety comments, + lints, and possible future language features? + +## Evidence + +- The project author required some form of prose safety justification to stand + in for selected Anneal proofs during incremental adoption. +- Existing Rust practice already locates human safety arguments near unsafe + operations, providing a migration source even though prose is not itself a + proof. + +## Links + +- [The TCB is explicit and shrinkable](0006-the-tcb-is-explicit-and-shrinkable.md) +- [Trust and incremental adoption](../open-questions/trust-and-incremental-adoption.md) +- [Rust safety integration](../open-questions/rust-safety-integration.md) diff --git a/anneal/agent_docs/design/decisions/0006-the-tcb-is-explicit-and-shrinkable.md b/anneal/agent_docs/design/decisions/0006-the-tcb-is-explicit-and-shrinkable.md new file mode 100644 index 0000000000..83a9c2fed4 --- /dev/null +++ b/anneal/agent_docs/design/decisions/0006-the-tcb-is-explicit-and-shrinkable.md @@ -0,0 +1,122 @@ + + +# 0006: The TCB is explicit and shrinkable + +- **Status:** Accepted +- **Date:** 2026-07-17 + +## Context + +Anneal cannot initially prove every layer on which a Rust execution depends. +Primitive unsafe operations, compiler intrinsics, FFI, assembly, the +verification toolchain, and hardware all introduce facts that may have to be +trusted. Hiding those assumptions behind a successful command would make the +result impossible to audit. + +At the same time, treating today's body-unmodeled operations as a permanent +semantic boundary would prevent future work from replacing them with formal +models. For example, a formal ISA model could eventually make some assembly +transparent. + +## Decision + +Anneal V2 will reduce unproved operational semantics to a small, explicit set +of trusted leaves and will expose the assumptions on which a result depends. +The TCB is an auditable boundary, not an implicit promise. + +Initially, trusted semantic leaves are expected to include some unsafe standard +library functions and intrinsics, raw-pointer dereferences, FFI, and inline or +external assembly. Approved axioms and prose justifications must remain visible +as unproved assumptions. Incomplete proofs must remain visible as outstanding +obligations; whether a particular command mode blocks on or conditionally +admits them remains open. None may masquerade as verified facts. + +The architecture must permit a trusted leaf or platform assumption to be +replaced by a more detailed formal model later. A fully adopted codebase should +reserve axioms for genuinely external semantics, although the boundary of +“external” can shrink as new models become available. + +This decision does not claim that Anneal's complete practical TCB is initially +small. The compiler, translators, proof checker, platforms, and hardware remain +part of the end-to-end TCB until independently justified. “Small” applies first +to the explicit set of trusted program-semantic leaves. + +## Rationale + +A small and inspectable trusted semantic leaf set, together with an explicit +account of the broader end-to-end TCB, lets a user understand exactly what an +Anneal result entitles them to believe. Making the boundary replaceable +supports stronger assurance over time without requiring the initial +implementation to formalize the Rust compiler, every ISA, and every foreign +system before it is useful. + +## Consequences + +- Verification results are relative to the correctness of their recorded + trusted leaves and platform assumptions. +- Anneal needs a TCB audit ledger which includes axioms and unfinished + obligations, not merely a binary success indicator. +- The ledger must ultimately account for relevant Anneal, Aeneas, Charon, + rustc, LLVM, host-hardware, and target-hardware assumptions; its exact schema + is not fixed here. +- Standard-library support may use the same axiom-authoring machinery exposed + for genuinely external user semantics. +- Replacing an axiom with a proof or a leaf with a model must reduce, rather + than merely relocate invisibly, the reported trust boundary. +- Anneal authors are responsible for the adequacy of built-in soundness + preconditions on axiomatic unsafe leaves. + +## Alternatives considered + +### Prove every leaf before V2 can be useful + +This would postpone practical verification until numerous independent compiler, +library, platform, and hardware models exist. + +### Trust arbitrary body-unmodeled functions without reporting them + +This would verify callers only relative to hidden assumptions and invite users +to overstate the result. + +### Make the initial leaf boundary permanent + +That would prevent stronger future models from reducing the TCB and would make +implementation expedience part of Anneal's long-term assurance definition. + +## Deferred questions + +- What is the exact TCB audit-ledger schema and output format? +- Which assumptions cause `cargo anneal verify` to fail, succeed conditionally, + or succeed with warnings? +- Which initial leaves are axiomatized by Anneal, Aeneas, a platform package, or + a user? +- Who authors and distributes FFI contracts: library consumers, upstream + library authors, or both? +- How are toolchain, host, target, and hardware identities represented? +- Which formal Rust, allocator, ISA, concurrency, and foreign-language models + should replace trusted leaves first? + +## Evidence + +- The project author defined V2's long-term direction as reducing the TCB to a + small explicit collection of trusted leaves while preserving the option to + model those leaves later. +- The project author identified the TCB audit log as an important user-facing + capability and required axioms and not-yet-proven specifications to appear in + it. +- The requested trust inventory includes Anneal's dependencies and both host + and target hardware, even though its exact schema remains open. + +## Links + +- [Verification is artifact-scoped](0002-verification-is-artifact-scoped.md) +- [Incremental adoption supports prose](0005-incremental-adoption-supports-prose-justifications.md) +- [Trust and incremental adoption](../open-questions/trust-and-incremental-adoption.md) +- [Source/model adequacy](../open-questions/source-model-adequacy.md) +- [Verification result and trust](../result-and-trust.md) diff --git a/anneal/agent_docs/design/decisions/README.md b/anneal/agent_docs/design/decisions/README.md new file mode 100644 index 0000000000..a231e49d52 --- /dev/null +++ b/anneal/agent_docs/design/decisions/README.md @@ -0,0 +1,60 @@ + + +# Design decisions + +This directory records Anneal V2 design decisions whose alternatives matter to +future work. A decision record says what was decided, why that choice follows +from Anneal's principles, and which questions it deliberately leaves open. + +Decision records complement, rather than replace, the other design documents: + +- [Principles](../principles.md) supplies reusable rules for evaluating design + alternatives. +- [Settled requirements](../settled-requirements.md) collects the constraints + that an acceptable design must satisfy. +- [Open questions](../open-questions/README.md) tracks design spaces in which no + choice has yet been made. + +An accepted record is normative until it is superseded. Historical evidence, +the V1 implementation, issues, and pull requests do not override it. If new +evidence changes a decision, add a new record that names the record it +supersedes instead of silently rewriting the old rationale. Small corrections +which do not change the decision may be made in place. + +## Statuses + +- **Proposed:** available for discussion, but not binding. +- **Accepted:** a current project commitment. +- **Rejected:** considered and deliberately not adopted. +- **Superseded:** retained as history, with a link to its replacement. + +## Authoring a record + +Copy [the template](0000-template.md), allocate the next four-digit number, and +keep the decision as narrow as the available evidence permits. In particular: + +- distinguish required outcomes from possible implementations; +- derive the rationale from project principles rather than precedent alone; +- list costs and constraints as well as benefits; +- move unresolved choices to **Deferred questions**; and +- link the evidence that made the decision possible. + +Do not turn a promising direction, an implementation trend, or a V1 design into +an accepted decision without explicit project agreement. + +## Accepted decisions + +| Record | Decision | +| --- | --- | +| [0001](0001-v2-is-a-clean-room-redesign.md) | V2 is a clean-room, ground-up redesign. | +| [0002](0002-verification-is-artifact-scoped.md) | A verification claim initially covers one fixed compilation artifact. | +| [0003](0003-expanded-generated-rust-is-input.md) | Expanded, generated Rust is verification input, not trusted source. | +| [0004](0004-invariants-support-all-property-kinds.md) | Type and trait invariants support arbitrary property kinds. | +| [0005](0005-incremental-adoption-supports-prose-justifications.md) | Incremental adoption supports explicit, audited prose justifications. | +| [0006](0006-the-tcb-is-explicit-and-shrinkable.md) | The trusted computing base is explicit, auditable, and shrinkable. | diff --git a/anneal/agent_docs/design/open-questions/README.md b/anneal/agent_docs/design/open-questions/README.md new file mode 100644 index 0000000000..ca5e098588 --- /dev/null +++ b/anneal/agent_docs/design/open-questions/README.md @@ -0,0 +1,76 @@ + + +# Open design questions + +This directory records consequential Anneal V2 design questions that have not +yet been decided. It exists to preserve the reasoning behind candidate designs +without turning the current implementation, Anneal V1, an issue, or a passing +conversation into policy by accident. + +An open question is not a blank slate. Each document begins with a compact +table linking the requirements and accepted decisions that constrain it, then +states only the topic-specific implications needed to evaluate candidates. +Those tables are indexes, not independent normative summaries. Agents and +humans may explore the remaining design space, but must not silently relax the +linked constraints. Conversely, candidates and current leanings are evidence +and working hypotheses, not commitments. + +The normative [project principles](../principles.md), +[settled requirements](../settled-requirements.md), and +[accepted decisions](../decisions/README.md) take precedence over this ledger. +Anneal V1 is a source of experience, not a default architecture for V2. When a +choice is accepted, record it in a decision record and update or close the +corresponding question here rather than merely changing an implementation. + +## Index + +| Area | Central question | +| --- | --- | +| [Property kinds and outcomes](property-kinds-and-outcomes.md) | How should Anneal represent distinct guarantees, execution outcomes, dependencies, and user selection without baking in a premature taxonomy? | +| [Rust safety integration](rust-safety-integration.md) | Which obligations should reuse Rust's `unsafe` machinery, and which require a richer Anneal-owned tracking system? | +| [Contracts and invariants](contracts-and-invariants.md) | How should function contracts, type invariants, and trait invariants be stated, enforced, and made available to callers? | +| [Source/model adequacy](source-model-adequacy.md) | How can proofs about a model that assumes soundness establish the soundness of the source program itself? | +| [Memory, resources, and effects](memory-resources-and-effects.md) | Where can unsafe implementations close to simple functional models, and where must resource or effect semantics remain visible? | +| [Trust and incremental adoption](trust-and-incremental-adoption.md) | How should axioms, incomplete proofs, prose justifications, and the audit ledger affect the meaning of verification? | +| [Aeneas and Charon integration](aeneas-charon-integration.md) | What information and machinery should Anneal consume, extend upstream, or own itself? | +| [Proof authoring and user experience](proof-authoring-and-user-experience.md) | What proof surface can eventually serve ordinary Rust engineers, formal-methods specialists, and agents without sacrificing rigor? | + +These areas intentionally overlap. A proposed answer should follow the related +links and account for its consequences elsewhere. In particular, choices about +property kinds affect Rust integration, contracts, trust reporting, and the +command-line interface; choices about source adequacy affect the Aeneas/Charon +boundary and the memory model. + +## How to update this ledger + +This section is the shared procedure for every page in this directory; +individual pages should add only topic-specific criteria and experiments. + +When adding evidence or a candidate design: + +1. State which settled constraints it preserves. +2. Distinguish observed facts from inferences and preferences. +3. Explain the user-visible and trusted-computing-base consequences. +4. Record dependencies on Rust, Lean, Aeneas, Charon, compilers, or hardware. +5. Prefer a small experiment or counterexample over confidence based only on + architectural taste. + +When deciding a question: + +1. Derive the decision from the project's principles and concrete evidence. +2. Add a decision record with alternatives and consequences. +3. Update every affected document, including settled requirements and current + state where appropriate. +4. Leave enough historical context here to explain what was learned, while + clearly marking the question or sub-question as resolved. + +Temporary disagreements about terminology should not be preserved as design +questions after the underlying meaning is understood. This ledger tracks real +choices that could change Anneal's guarantees, architecture, or user +experience—not conversational cleanup. diff --git a/anneal/agent_docs/design/open-questions/aeneas-charon-integration.md b/anneal/agent_docs/design/open-questions/aeneas-charon-integration.md new file mode 100644 index 0000000000..0df6ba07ba --- /dev/null +++ b/anneal/agent_docs/design/open-questions/aeneas-charon-integration.md @@ -0,0 +1,151 @@ + + +# Aeneas and Charon integration + +**Status:** Open design discussion. + +Anneal is intended to orchestrate and extend Charon's compiler extraction and +Aeneas's Lean translation. V2 must decide which interfaces to consume, which +capabilities to add upstream, and which temporary adaptations Anneal should +own. These are engineering choices governed by semantic fidelity, +maintainability, and user experience rather than a categorical ownership rule. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-001](../settled-requirements.md#anneal-req-001-v2-is-a-clean-room-redesign), [decision 0001](../decisions/0001-v2-is-a-clean-room-redesign.md) | V1 integration techniques carry no presumption into V2. | +| [ANNEAL-REQ-017](../settled-requirements.md#anneal-req-017-initial-claims-are-artifact-scoped), [decision 0002](../decisions/0002-verification-is-artifact-scoped.md) | Integration must identify one compiler-resolved compilation subject. | +| [ANNEAL-REQ-018](../settled-requirements.md#anneal-req-018-generated-rust-is-analyzed-input), [decision 0003](../decisions/0003-expanded-generated-rust-is-input.md) | Expanded generated Rust which enters the artifact is analyzed input. | +| [ANNEAL-REQ-019](../settled-requirements.md#anneal-req-019-coverage-adequacy-is-enforced) | Every potentially invalid operation in the reported coverage envelope must be reconciled with complete obligation coverage. | +| [ANNEAL-REQ-021](../settled-requirements.md#anneal-req-021-results-carry-an-audit-ledger) | Results must record the relevant translator, compiler, and proof-tool identities and gaps. | +| [ANNEAL-REQ-025](../settled-requirements.md#anneal-req-025-existing-proof-machinery-is-preferred), [ANNEAL-REQ-026](../settled-requirements.md#anneal-req-026-upstream-evolution-is-in-scope) | Suitable maintained machinery is preferred, and upstream changes are available when they are the best engineering choice. | + +Topic-specific implications: + +- The compiler-resolved artifact must remain authoritative. Any source scanner, + annotation index, generated proof, or sidecar manifest must reconcile with + it rather than silently creating a shadow view of the Rust program. +- No requirement categorically assigns a capability upstream or downstream. + Ownership depends on semantic fidelity, interface robustness, maintenance + burden, and user experience. +- Direct LLBC consumption, structured compiler metadata, Lean syntax + extensions, and downstream adapters all remain candidates. Fragile textual + rewriting is evidence that an interface may be missing, not a prohibited + implementation technique. + +V1's duplicate progress and conditional-correctness proofs are evidence in +favor of experimenting with Aeneas's WP specifications and `step`/`step*` +tactics. They do not settle the proof architecture. + +## Information boundary + +LLBC is a natural semantic input because Charon has already resolved much of +Rust's syntax and types. Anneal annotations also need to bind source intent to +the exact items, fields, operations, and calls that the compiler verifies. +Depending only on a parallel `syn` parse risks creating a shadow view that +disagrees after macro expansion, `cfg` processing, name resolution, or +desugaring. + +One candidate is a compiler-resolved annotation or index mode in Charon. It +could expose expanded annotations, stable-within-artifact item identifiers, +signatures, source provenance, monomorphized or resolved call metadata, unsafe +operations, field accesses, and links to LLBC declarations. A source scanner +could remain a bootstrap or authoring aid but would have to reconcile exactly +against this authoritative index. + +This candidate has not been accepted. Its motivation is to avoid silent skew, +support generated code, find every obligation, improve diagnostics, and reduce +dependence on generated Lean names. We still need to determine which facts are +already in LLBC, which should be added to Charon, and which Anneal can derive +reliably. + +## Questions to resolve + +### What should Charon expose? + +- How are annotations preserved through expansion and lowering? +- Which identifiers remain stable enough for proof artifacts, incremental + builds, and diagnostics? +- Can fields, unsafe operations, drop glue, trait dispatch, closures, and + compiler-generated items be indexed uniformly? +- Does Anneal need MIR-level facts that LLBC intentionally omits? +- How are source spans represented for macro-generated and desugared code? +- Can Charon report unsupported or erased constructs so Anneal fails closed? +- At what compiler phase must extraction occur to avoid transformations that + assume undefined behavior cannot happen? + +The last question is part of the adequacy problem described in +[source/model adequacy](source-model-adequacy.md). + +### What should Aeneas expose or own? + +- Can unsafe leaves be represented within Aeneas's WP semantics with explicit + guards and resource effects? +- Which distinctions among return, panic, unwind, abort, divergence, undefined + operation, and modeling failure should Aeneas preserve? +- How can multiple property obligations share symbolic execution through + `step` and `step*` without forcing every domain into the same logic? +- What changes are needed for separation-logic objects or capabilities whose + use must remain affine or linear? +- Should Aeneas emit structured proof metadata alongside Lean definitions? +- Can generated definitions expose stable theorem interfaces rather than + implementation-specific names? +- How does unsafe and separation-logic work available or proposed in the + relevant Aeneas revision relate to an Anneal-owned short-term pointer model? + +Generic resource machinery may belong in Lean libraries, Rust-specific +semantics in Aeneas, and orchestration in Anneal, but that division is only a +working possibility. See [memory, resources, and effects](memory-resources-and-effects.md). + +### How does Anneal attach its contracts? + +Candidate techniques include: + +- extend LLBC with elaborated contracts and invariant declarations; +- provide Aeneas a structured sidecar manifest keyed by Charon identifiers; +- extend Aeneas lowering so proposition-valued contract arguments appear in + generated functions; +- generate sidecar WP theorems for every indexed call; +- inject stable Lean macros or syntax that elaborate against generated + declarations; and +- validate generated Lean against an independent obligation manifest. + +The choice should be based on completeness, auditability, compatibility with +Aeneas tactics, diagnostic quality, and maintenance cost. “No textual +post-processing ever” is not a principle, but fragile search-and-replace over +generated code is strong evidence that an upstream interface is missing. + +### How are versions and downstream adaptations managed? + +- Does Anneal track released Aeneas/Charon versions, pinned revisions, or a + maintained fork? +- What compatibility contract can upstream realistically offer? +- How do proof artifacts record the exact translator and standard-library + versions they depend on? +- When should experimental work live downstream before an upstream API is + proposed? +- Who owns tests demonstrating that an upstream change preserves Anneal's + semantic assumptions? + +## Evaluation criteria + +A durable integration must make the compiler-resolved artifact authoritative, +detect annotation or coverage skew, preserve all semantics needed for claimed +properties, and give proof authors stable interfaces. It should reuse upstream +machinery, avoid imposing Anneal-only complexity on all Aeneas users, and leave +a credible path for temporary downstream work to mature upstream. + +Useful experiments include a proc-macro-generated unsafe call with an +annotation, a generic trait call resolved after monomorphization, an invariant +on a compiler-generated field access path, shared WP execution for two property +kinds, and a resource assertion that Lean cannot duplicate. + +The effect on ordinary users is discussed in +[proof authoring and user experience](proof-authoring-and-user-experience.md). diff --git a/anneal/agent_docs/design/open-questions/contracts-and-invariants.md b/anneal/agent_docs/design/open-questions/contracts-and-invariants.md new file mode 100644 index 0000000000..58733f32c4 --- /dev/null +++ b/anneal/agent_docs/design/open-questions/contracts-and-invariants.md @@ -0,0 +1,176 @@ + + +# Contracts and invariants + +**Status:** Open design discussion. + +Function contracts, type invariants, and trait invariants are the principal +units by which local proofs become reusable facts. Their semantic roles are +durable, but their syntax, enforcement mechanisms, and relationship to Rust's +types remain open for V2. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational), [ANNEAL-REQ-006](../settled-requirements.md#anneal-req-006-soundness-specifications-produce-adequate-obligations) | User contracts cannot weaken or erase Rust soundness obligations. | +| [ANNEAL-REQ-009](../settled-requirements.md#anneal-req-009-local-contract-obligations), [ANNEAL-REQ-010](../settled-requirements.md#anneal-req-010-local-results-compose-globally) | Item contracts must support local proof and reusable global composition. | +| [ANNEAL-REQ-012](../settled-requirements.md#anneal-req-012-property-dependencies) | Contracts and invariants must express dependencies among property kinds, including cycles treated soundly. | +| [ANNEAL-REQ-014](../settled-requirements.md#anneal-req-014-type-invariants-support-arbitrary-property-kinds), [ANNEAL-REQ-015](../settled-requirements.md#anneal-req-015-trait-invariants-support-arbitrary-property-kinds), [decision 0004](../decisions/0004-invariants-support-all-property-kinds.md) | Both type and trait invariants support arbitrary property kinds, with their respective establishment and use obligations enforced. | +| [ANNEAL-REQ-016](../settled-requirements.md#anneal-req-016-contracts-distinguish-semantic-roles) | The model must distinguish soundness obligations from ordinary functional preconditions and other property roles. | +| [ANNEAL-REQ-019](../settled-requirements.md#anneal-req-019-coverage-adequacy-is-enforced) | Whatever contract encoding is chosen must not omit a potentially invalid operation within the reported coverage envelope. | + +Topic-specific implications: + +- A safe API cannot make undefined behavior depend on an extra unchecked + obligation of its safe caller. It may still state conditional functional or + other guarantees without turning their conditions into soundness + preconditions. +- Built-in soundness contracts are answerable to Rust's semantics. A + user-defined correctness axiom records the user's intended property; Anneal + can enforce and report it but cannot supply its real-world intent. +- V1's `isValid`, `isSafe`, and indentation-sensitive proof syntax are neither + enforcement mechanisms nor syntax commitments for V2. + +## Function contracts + +### Safety contracts versus general contracts + +Rust's source syntax does not distinguish a soundness precondition from a +precondition for panic freedom, a functional result, or a protocol. V2 needs a +semantic distinction even if the surface syntax is shared. + +Questions include: + +- Does every clause name its property kind explicitly, inherit one from its + declaration, or elaborate to a typed Lean-level obligation? +- How does a safe function express “if `x > 0`, the result has property P” + without suggesting that `x <= 0` may cause undefined behavior? +- Can a single precondition support multiple postconditions or property kinds? +- How are frame conditions, exceptional postconditions, trace conditions, and + resource transfer represented? +- Are contracts attached to source functions, monomorphized instances, trait + methods, function values, or compiler-resolved items with quantified + generics? +- Which contract facts become part of a separately compiled crate's + verification interface? + +The surface should make an accidental weakening of soundness obligations hard +to overlook while remaining usable for general correctness claims. + +### Contracts as types or sidecar theorems + +One candidate lowers a Rust function with Anneal preconditions to a Lean +function whose proposition-valued arguments must be supplied at every call. +This closely resembles an extension to the type system and makes an omitted +proof ill-typed. Another keeps Aeneas's ordinary function model and proves +sidecar theorems showing that every call satisfies the relevant contract. The +latter aligns more directly with existing Aeneas WP machinery. + +This is primarily a representation and enforcement choice. Either is +acceptable only if Anneal can establish complete coverage of all applicable +calls. The deeper circularity in using a soundness-dependent model is treated +in [source/model adequacy](source-model-adequacy.md). + +Open details include higher-order calls, recursion, dynamic dispatch, trait +resolution, closures, foreign calls, and how proof obligations survive +monomorphization or separate compilation. + +## Type invariants + +A type invariant describes facts that valid uses of a value may rely on. It may +support soundness—for example, initialized storage or a valid pointer +relationship—or another property such as a cryptographic representation +invariant or resource bound. + +Questions include: + +- Is an invariant a proposition over an abstract value, a resource assertion, + a family indexed by property kind, or an interface that can provide multiple + forms of evidence? +- At which points must it hold: all observable safe states, function + boundaries, borrow boundaries, suspension points, panic edges, or some + declared subset? +- How is an invariant opened temporarily, and what capability guarantees that + it is restored before control escapes through return, panic, cancellation, + or destruction? +- Which reads require proof that the invariant holds, and which writes require + proof that it is re-established? +- How do interior mutability, aliasing, pinning, drop, partial initialization, + unions, and concurrency change the proof rules? +- Can a type carry several invariants with dependencies between property kinds? + +Enforcement might build on Rust unsafe fields or use Anneal-specific analysis; +see [Rust safety integration](rust-safety-integration.md). Resource-bearing +invariants cannot be flattened into freely duplicable propositions; see +[memory, resources, and effects](memory-resources-and-effects.md). + +## Trait invariants + +The durable idea behind V1's `isSafe` is that an implementation supplies an +invariant promised by the trait, and generic code consumes that invariant from +a known bound. V2 must make both halves enforceable. + +Questions include: + +- Does the trait declare one invariant per property kind, one structured family + of invariants, or named obligations with explicit dependencies? +- Which implementations require a proof: unsafe implementations only, all + implementations of an annotated trait, or a set selected by the property? +- How is evidence made available in a generic context with `T: Trait`? +- How are associated types, constants, generic associated types, supertraits, + negative reasoning, specialization, and trait objects handled? +- Does dynamic dispatch carry a proof dictionary, rely on a sidecar theorem for + the vtable, or elaborate through another mechanism? +- How do auto traits and compiler-generated implementations participate? +- Can an implementation assume other property-kind obligations while proving + its own, and how are cycles certified? + +The answer must prevent an implementation from entering verified code without +its declared obligations while avoiding repeated proofs at every generic use. + +## Specification adequacy and evolution + +Lean can prove a weak or vacuous proposition. For non-axiomatic soundness +specifications, Anneal must connect generated obligations to modeled primitive +semantics strongly enough to guarantee adequacy; human review alone is not the +end state. How it does so is open. + +For user-defined properties, specification intent ultimately comes from the +user. Anneal can still help by detecting unused clauses, vacuous implications, +inconsistent assumptions, or contracts that do not cover executions, but such +checks do not create an external ground truth. + +Contracts also need an evolution story: + +- What changes are compatible for downstream proofs? +- Can implementation details and Aeneas-generated names remain hidden behind a + stable verification interface? +- How are property-kind dependencies versioned? +- Can automated proof repair absorb small Rust refactorings without concealing + a semantic contract change? + +## Evaluation criteria and examples + +A viable design must preserve safe Rust's soundness promise, enforce every +declared implementation obligation, expose exactly the facts a caller may use, +respect resource semantics, and compose across generics and crates. + +Representative experiments should cover: + +- a safe API around a raw-pointer representation; +- a safe function with a conditional functional guarantee but no caller + soundness obligation; +- a type whose field invariant is temporarily broken and restored; +- an unsafe trait with generic and dynamically dispatched consumers; +- a trait invariant for a property other than soundness; and +- mutually dependent type, trait, and callee properties. + +Proof surface and diagnostics are discussed in +[proof authoring and user experience](proof-authoring-and-user-experience.md). diff --git a/anneal/agent_docs/design/open-questions/memory-resources-and-effects.md b/anneal/agent_docs/design/open-questions/memory-resources-and-effects.md new file mode 100644 index 0000000000..618f709c90 --- /dev/null +++ b/anneal/agent_docs/design/open-questions/memory-resources-and-effects.md @@ -0,0 +1,159 @@ + + +# Memory, resources, and effects + +**Status:** Open design discussion. + +Aeneas obtains a simple functional model for a large subset of Rust by using +the borrow checker's discipline. Unsafe Rust, interior mutation, allocators, +concurrency, I/O, and similar features can require spatial, temporal, or +effectful reasoning. Anneal's central opportunity is to combine the simple +functional domain with enough resource-aware machinery to verify unsafe code +without imposing a full heap logic on every proof. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-003](../settled-requirements.md#anneal-req-003-general-rust-use-cases) | The architecture must accommodate Rust domains whose essential memory, concurrency, or external-effect semantics cannot be erased. | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational) | Simplicity cannot weaken the soundness foundation of a source-level claim. | +| [ANNEAL-REQ-007](../settled-requirements.md#anneal-req-007-the-memory-model-is-conservative) | Any Anneal-owned memory model must conservatively formalize the normative Rust guarantees it claims. | +| [ANNEAL-REQ-008](../settled-requirements.md#anneal-req-008-resource-semantics-are-preserved) | Ownership, provenance, initialization, permissions, and protocol resources must retain their usage discipline in Lean. | +| [ANNEAL-REQ-010](../settled-requirements.md#anneal-req-010-local-results-compose-globally) | Resource and effect reasoning must support abstraction boundaries whose established contracts are reusable by callers. | +| [ANNEAL-REQ-011](../settled-requirements.md#anneal-req-011-long-running-and-exceptional-behavior) | The model must support invariant-preserving infinite execution and sound panic, unwind, and recovery paths. | +| [ANNEAL-REQ-025](../settled-requirements.md#anneal-req-025-existing-proof-machinery-is-preferred), [ANNEAL-REQ-026](../settled-requirements.md#anneal-req-026-upstream-evolution-is-in-scope) | Suitable maintained machinery is preferred, but Anneal, Aeneas, Charon, Lean libraries, and Rust may evolve where needed. | + +Topic-specific implications: + +- Prefer the simplest abstraction that preserves every fact needed for the + claim. Pure value contracts are desirable when faithful, but purity is not + an independent objective. +- Operationally global state or history may be packaged behind local + capabilities, shared invariants, or abstract interfaces only if the proof + rules preserve its resource discipline. +- Robust contextual refinement at a safe boundary does not require literal + representation as a pure value transformer. Effectful, world-indexed, or + protocol interfaces remain available when a simpler boundary would erase + claim-relevant behavior. + +## Locality and abstraction closure + +Safe encapsulation demonstrates that unsafe implementation details can often +be hidden behind a safe interface: clients should not need to reason about the +entire program to use a well-designed abstraction soundly. Separation logic +recovers a related locality by splitting global state into composable resources. +Anneal should exploit this symmetry, but must not assume every abstraction can +be represented as a pure function on values. + +Open questions include: + +- What semantic condition shows that an unsafe implementation refines its safe + interface in every safe context? +- Which effects can close behind an existential representation invariant, and + which must remain in the public contract? +- Can allocator state, provenance history, concurrency protocols, and device + state be represented by local capabilities or shared invariants? +- When a fact is operationally global, what proof rules let a client use a + localized view without making the proof unsound? +- How are abstraction boundaries nested and composed across crates? + +The objective is not purity for its own sake. It is the simplest interface that +is faithful, compositional, understandable, and resilient to implementation +change. + +## Questions to resolve + +### What resource logic is required? + +- Which assertions must be affine, linear, persistent, fractional, or otherwise + controlled? +- How are allocation, initialization, validity, provenance, aliasing, + permissions, and lifetime represented? +- Which rules are generic separation-logic infrastructure and which encode + Rust-specific semantics? +- Can Aeneas's existing state and WP machinery host these assertions, or is a + new monad or logic required? +- How are resource assertions transferred through Aeneas's forward/backward + treatment of borrows? +- How do resource obligations appear in ordinary Lean goals and tactics without + letting users duplicate or discard them illegally? + +The design should reuse maintained Lean and Aeneas abstractions wherever they +fit. Reinvention remains possible when an existing abstraction cannot express +the needed guarantee or would impose unacceptable complexity. + +### Which effects remain visible? + +Representative domains include: + +- allocators and address reuse; +- I/O and interaction with an external environment; +- atomics, locks, threads, and scheduling; +- nondeterminism and randomness; +- panic, unwind cleanup, cancellation, and abort; +- volatile or memory-mapped operations; +- FFI and inline or out-of-line assembly; and +- long-running services and reactive protocols. + +For each, V2 must decide whether a boundary exposes a state transformer, an +effect trace, a WP, a protocol capability, a nondeterministic relation, or a +simpler derived contract. The answer may vary by property kind. A functional +result theorem may hide scheduling details that a deadlock theorem must retain. + +### How conservative is the memory model? + +Rust's operational guarantees are still largely written in prose and continue +to evolve. V2 must determine: + +- which normative documents and team decisions ground each axiom; +- how ambiguity is handled without accidentally claiming more than Rust + guarantees; +- when to ask the Rust project to clarify or change the reference; +- how target layout, ABI, compiler, and hardware assumptions enter the model; +- how provenance and aliasing rules are versioned; and +- how proofs remain useful as the model is refined. + +The authors' direct involvement with Rust's operational-semantics work makes +upstream clarification possible. It does not remove the need to expose current +assumptions in Anneal's trust ledger. + +### Where should the implementation live? + +Candidate arrangements include: + +- Aeneas owns general unsafe or separation-logic semantics and Anneal supplies + annotations and orchestration; +- Anneal temporarily owns a conservative pointer/layout layer that later moves + upstream; +- Lean libraries own generic resource machinery while Aeneas owns Rust + instantiations; and +- multiple semantic backends coexist behind a common contract interface. + +Changes should be upstream when they form reusable Aeneas or Charon +functionality and when the maintenance burden is acceptable. Shipping a sound +and auditable Anneal remains more important than an aesthetically perfect +ownership boundary. + +## Evaluation criteria + +A candidate must preserve resource usage rules, support modular composition, +state its relationship to normative Rust, and make exceptional and infinite +executions sound. It should keep simple safe-code proofs simple and reveal +complex machinery only where the claimed behavior needs it. It should also +allow the trusted model to shrink or become more precise without rewriting +unrelated user proofs. + +Useful experiments include a raw-pointer container that closes to a pure safe +API, an allocator whose capability must remain visible, a lock with a shared +invariant, panic during partially initialized construction, and an I/O protocol +whose functional return value alone is inadequate. + +See also [property kinds and outcomes](property-kinds-and-outcomes.md), +[contracts and invariants](contracts-and-invariants.md), and +[Aeneas and Charon integration](aeneas-charon-integration.md). diff --git a/anneal/agent_docs/design/open-questions/proof-authoring-and-user-experience.md b/anneal/agent_docs/design/open-questions/proof-authoring-and-user-experience.md new file mode 100644 index 0000000000..c8efa210fa --- /dev/null +++ b/anneal/agent_docs/design/open-questions/proof-authoring-and-user-experience.md @@ -0,0 +1,177 @@ + + +# Proof authoring and user experience + +**Status:** Open design discussion. + +Anneal's eventual audience includes ordinary Rust teams, formal-methods +specialists, and coding agents. The aspiration is that even early-career Rust +engineers can participate, potentially with AI assistance, while the resulting +claims remain rigorous and reviewable. The right source syntax, proof workflow, +and division of labor are matters for experimentation. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-001](../settled-requirements.md#anneal-req-001-v2-is-a-clean-room-redesign), [decision 0001](../decisions/0001-v2-is-a-clean-room-redesign.md) | V1's literate proof syntax is evidence, not a product commitment. | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational), [ANNEAL-REQ-021](../settled-requirements.md#anneal-req-021-results-carry-an-audit-ledger) | A smoother interface cannot weaken the formal claim or conceal its dependencies. | +| [ANNEAL-REQ-010](../settled-requirements.md#anneal-req-010-local-results-compose-globally) | Established abstraction contracts must be reusable without reopening private bodies. | +| [ANNEAL-REQ-022](../settled-requirements.md#anneal-req-022-incremental-adoption-supports-prose), [decision 0005](../decisions/0005-incremental-adoption-supports-prose-justifications.md) | The workflow must accommodate explicit, audited prose justifications during incremental adoption. | +| [ANNEAL-REQ-024](../settled-requirements.md#anneal-req-024-incompleteness-is-distinguishable-from-external-trust) | UX and diagnostics must not collapse unfinished proofs into intentional external trust. | +| [ANNEAL-REQ-025](../settled-requirements.md#anneal-req-025-existing-proof-machinery-is-preferred) | Suitable Lean and Aeneas machinery should be reused rather than rebuilt without a concrete benefit. | +| [ANNEAL-REQ-027](../settled-requirements.md#anneal-req-027-ordinary-rust-engineers-are-a-target-audience) | The eventual workflow must serve ordinary Rust engineers without sacrificing meaning or auditability. | + +Topic-specific implications: + +- Machine checking, not trust in a human- or AI-generated explanation, + establishes a formal claim. Assistance can change who writes a proof, but + not what counts as evidence. +- Proof interfaces should avoid needless dependence on generated names and + internal WP structure. That preference does not require hiding Lean or + Aeneas from expert users. +- Humans and agents should work from the same contracts, principles, and + result semantics even when their authoring interfaces differ. + +## Who authors what? + +Possible workflows include: + +- Rust engineers write contracts and proof-relevant explanations while agents + synthesize Lean proofs; +- agents propose both code and specifications, with humans reviewing intent and + Lean checking proof correctness; +- formal-methods specialists publish reusable contracts, tactics, and models + consumed by ordinary teams; +- library authors ship verified interfaces that downstream users consume + without seeing implementation proofs; and +- humans write all proof material directly for especially sensitive code. + +V2 should not assume one universal workflow. It should identify which artifacts +require human judgment—especially the intended meaning of user-defined +specifications—and which can be generated or checked mechanically. + +Open questions include: + +- What must a Rust author understand about Lean, LLBC, Aeneas WP semantics, and + memory resources? +- Which proof steps are stable enough for agents to regenerate automatically? +- How does review distinguish a semantic specification change from proof repair + after a refactor? +- Can organizations require human approval of axioms or soundness contracts + while automating ordinary proofs? +- How are proof ownership and maintenance responsibility recorded? + +## Surface syntax and artifact layout + +Candidate locations include Rust attributes, doc comments, inline comments, +adjacent Lean files, generated proof modules with checked-in overlays, or a +combination. Each has different consequences for macro expansion, IDE support, +source control, Rust documentation, and proof reuse. + +Questions to resolve: + +- How are property kinds, preconditions, postconditions, type invariants, trait + invariants, exceptional behavior, and resource transfer written? +- Which parts use Rust-like syntax and which expose Lean terms? +- Can specifications remain near Rust while larger proofs live in ordinary Lean + modules? +- How does a proof refer to compiler-resolved items without depending on + unstable generated names? +- Are proofs checked in, generated on demand, cached as artifacts, or all three + under different policies? +- How are macro-generated items annotated or given contracts? +- Can source formatting and rustdoc ignore Anneal content cleanly? +- What is the migration path if syntax evolves rapidly during pre-alpha work? + +The compiler binding needed for these choices is discussed in +[Aeneas and Charon integration](aeneas-charon-integration.md). + +## Obligation presentation and diagnostics + +`cargo anneal verify` should help a Rust engineer understand what must be true +at the relevant source location. It remains open how much of the underlying +Lean goal and Aeneas state is exposed. + +Useful diagnostic capabilities may include: + +- a Rust-level explanation of the violated callee precondition; +- the property kind and transitive dependency that generated it; +- the exact compiler-resolved operation, including generated code provenance; +- relevant assumptions, type or trait invariants, and owned resources; +- the normal, panic, unwind, or other path on which the obligation occurs; +- a minimal Lean goal for expert debugging; +- an audit distinction among failed, unsupported, incomplete, axiomatic, and + prose-justified obligations; and +- machine-readable output for IDEs and agents. + +Questions include whether Anneal should synthesize counterexamples, symbolic +traces, suggested invariants, or proof skeletons; how it avoids presenting an +unsoundly simplified explanation; and how diagnostics remain stable when +Aeneas internals change. + +## Verification loop + +The desired workflow should feel proportionate to ordinary Rust development: +fast feedback for local changes, a stronger reproducible check in CI, and a +clear audit artifact for review or release. Design work is needed for: + +- incremental extraction and Lean recompilation; +- caching keyed by the exact Cargo artifact and toolchain; +- checking selected property kinds and their dependencies; +- distinguishing quick local checking from release assurance without + overloading “verified”; +- editing support that navigates between Rust obligations and Lean proofs; +- proof repair when generated definitions change; and +- reducing irrelevant churn in error messages and audit logs. + +The command success policy is part of +[trust and incremental adoption](trust-and-incremental-adoption.md), while the +semantics of selected properties are covered in +[property kinds and outcomes](property-kinds-and-outcomes.md). + +## Abstraction and leakage + +Some Aeneas concepts will inevitably be useful to proof authors. The open +question is which become stable Anneal concepts and which remain expert escape +hatches. + +Candidate layers include: + +1. Rust-oriented contracts and generated obligations for common proofs. +2. Reusable Anneal tactics and libraries that expose selected WP and resource + concepts. +3. Full Lean and Aeneas access for specialists and novel domains. + +This layering is only a candidate. It must not cause the convenient layer to +hide assumptions or make advanced properties impossible. Likewise, forcing all +users to manipulate generated forward/backward functions or raw separation +logic would undermine the broad-adoption goal if stable abstractions can avoid +it. + +## Evaluation criteria and experiments + +Evaluate workflows by semantic clarity, error discoverability, proof stability, +auditability, adoption cost, and the ability of both humans and agents to make +safe changes. Raw proof length or the absence of visible Lean is not by itself a +measure of usability. + +Experiments should include: + +- a new Rust graduate repairing a failed call-site proof with guided tooling; +- an agent updating a proof after a small implementation refactor without + changing the contract; +- a specialist adding a new resource-aware property domain; +- migration from `// SAFETY:` prose to a formal proof; +- review of a PR that changes both a contract and its proof; and +- downstream use of a verified generic library without dependence on generated + Aeneas names. + +The governing contract and invariant questions are recorded in +[contracts and invariants](contracts-and-invariants.md). diff --git a/anneal/agent_docs/design/open-questions/property-kinds-and-outcomes.md b/anneal/agent_docs/design/open-questions/property-kinds-and-outcomes.md new file mode 100644 index 0000000000..0c14ee4b3e --- /dev/null +++ b/anneal/agent_docs/design/open-questions/property-kinds-and-outcomes.md @@ -0,0 +1,164 @@ + + +# Property kinds and execution outcomes + +**Status:** Open design discussion. + +Anneal must reason about Rust soundness and also support properties such as +panic freedom, deadlock freedom, cryptographic correctness, protocol +correctness, and resource bounds. Rust's present `safe`/`unsafe` distinction +does not identify these different kinds of obligation. V2 needs an extensible +model, but adopting a taxonomy too early would constrain domains that have not +yet been explored. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-002](../settled-requirements.md#anneal-req-002-general-properties), [ANNEAL-REQ-004](../settled-requirements.md#anneal-req-004-extensibility-before-breadth) | The architecture must admit arbitrary user-defined property domains without requiring all specialized backends initially. | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational) | Soundness is a mandatory semantic foundation, not an optional peer of user-selected properties. | +| [ANNEAL-REQ-009](../settled-requirements.md#anneal-req-009-local-contract-obligations), [ANNEAL-REQ-010](../settled-requirements.md#anneal-req-010-local-results-compose-globally) | Property evidence must support local proof and global composition. | +| [ANNEAL-REQ-011](../settled-requirements.md#anneal-req-011-long-running-and-exceptional-behavior) | Verification cannot equate success with normal termination; it must express invariant-preserving divergence and sound panic, unwind, and recovery. | +| [ANNEAL-REQ-012](../settled-requirements.md#anneal-req-012-property-dependencies) | Property kinds may depend on one another, including through cycles that require a sound joint treatment. | +| [ANNEAL-REQ-013](../settled-requirements.md#anneal-req-013-property-selection) | Users must eventually be able to select which non-foundational properties are enforced. | +| [ANNEAL-REQ-014](../settled-requirements.md#anneal-req-014-type-invariants-support-arbitrary-property-kinds), [ANNEAL-REQ-015](../settled-requirements.md#anneal-req-015-trait-invariants-support-arbitrary-property-kinds), [decision 0004](../decisions/0004-invariants-support-all-property-kinds.md) | Both invariant forms must carry arbitrary property kinds. | + +Topic-specific implications: + +- Selecting or defining another property cannot substitute for the soundness + obligations needed to interpret its theorem as a claim about Rust. +- A common execution model may share evidence among properties, but no + requirement forces domains with different semantics into identical proof + judgments. +- The taxonomy, dependency algorithm, cycle treatment, and command/reporting + vocabulary all remain open. + +## Taxonomy remains open + +One proposal distinguishes: + +- semantic outcomes and effects, such as return, panic or unwind, abort, + divergence, undefined behavior, and model or tool failure; +- standard assurance policies, such as soundness, panic freedom, termination, + partial correctness, and total correctness; and +- extensible user property domains, such as functional, relational, trace, + protocol, quantitative, or probabilistic properties. + +This proposal has deliberately been neither accepted nor rejected. These terms +are useful for exploring the space, but must not be exposed as a stable API or +used to infer settled semantics. Among other issues, a property like deadlock +freedom may concern traces, progress, concurrency resources, and termination at +once; “panic freedom” may need to distinguish panic, abort, and unwind; and the +boundary between a policy and a user domain may not survive real examples. + +## Questions to resolve + +### What is first-class? + +- Which concepts, beyond soundness, should Anneal itself understand? +- Should panic, unwind, abort, nontermination, and ordinary return be modeled as + outcomes, effects, predicates over traces, or some combination? +- Which concepts need dedicated compiler extraction or proof machinery, and + which can be libraries defined over a smaller semantic core? +- Can one representation cover safety properties, liveness properties, + hyperproperties, probabilistic claims, and quantitative bounds without + pretending that their proof rules are identical? + +Initial V2 is expected to supply an extensible architecture rather than +complete support for deadlock freedom, hyperproperties, quantitative bounds, +or cryptographic reasoning. + +### How are execution paths combined? + +V1 split “progress” from conditional correctness. Experience suggests that the +split duplicated symbolic-execution work and fit poorly with Aeneas's WP +specifications and `step`/`step*` tactics. The current direction is to build on +Aeneas's combined machinery and share symbolic execution across obligations. +It remains open: + +- how path-specific obligations are attached to normal return, panic, unwind, + abort, and unbounded execution; +- whether different property kinds consume a common execution certificate or + require domain-specific proof judgments; +- how cleanup during unwinding is modeled well enough to establish soundness; + and +- how partial or total correctness is requested without making soundness + depend on termination. + +The Aeneas revision examined during this design discussion represented several +exceptional situations through a coarse failure channel. A bounds check, +arithmetic overflow, explicit panic, undefined operation, unsupported model +feature, and tool failure can have very different implications. Before relying +on this observation, recheck the Aeneas revision pinned by the current +toolchain. We still need to determine which cases it combines, which +distinctions survive LLBC lowering, and whether to refine the semantic result +type, attach metadata, or express the distinctions in WP predicates. This is an +investigation, not a claim about the correct Aeneas API. + +### How do dependencies compose? + +- How are dependencies between property kinds declared and discovered? +- Should selecting a property automatically select its transitive dependency + closure? +- If a dependency is excluded, does verification fail, succeed relative to an + audited assumption, or vary by command profile? +- How should mutually dependent properties be proven? Candidate approaches + include an explicit joint certificate for each strongly connected component, + inductive closure, and coinductive closure for appropriate liveness claims. +- How are dependencies represented through generic functions, trait bounds, + dynamic dispatch, and separately verified crates? + +These choices interact with the meaning of an incomplete proof and with trust +reporting; see [trust and incremental adoption](trust-and-incremental-adoption.md). + +### What does the user select and see? + +- Are property kinds named globally, scoped to crates, or identified by Lean + propositions or Rust declarations? +- Can projects define new kinds with reusable proof rules, or only attach + arbitrary propositions to built-in mechanisms? +- Does a command select desired top-level guarantees, obligations to check, or + both? +- How should output distinguish “not requested,” “proved,” “assumed,” “blocked + by unsupported semantics,” and “not applicable”? +- Which guarantees belong in machine-readable artifacts so downstream crates + can rely on them? + +## Evaluation criteria + +An acceptable design must: + +1. Make it impossible to interpret another selected property as a + substitute for soundness. +2. Give panic, divergence, and recovery faithful meanings rather than treating + them all as failed verification or silently discarding their paths. +3. Preserve compositional reasoning across functions and crates. +4. Avoid performing essentially the same symbolic execution independently for + every property where evidence can safely be shared. +5. Allow specialized proof systems where sharing would erase a domain's + semantics. +6. Produce an audit result whose dependencies and assumptions a user can + understand. +7. Be testable on realistic examples before the vocabulary becomes stable. + +## Useful experiments + +- A server loop that maintains an invariant forever without promising + termination. +- A destructor that runs during unwinding and whose unsafe operations must + remain sound. +- A function whose soundness depends on a callee's cryptographic or protocol + property. +- A lock abstraction with mutually dependent ownership and deadlock claims. +- One implementation checked for soundness, panic freedom, and a functional + result property using shared symbolic execution. + +Related questions include [Rust safety integration](rust-safety-integration.md), +[memory, resources, and effects](memory-resources-and-effects.md), and +[proof authoring](proof-authoring-and-user-experience.md). diff --git a/anneal/agent_docs/design/open-questions/rust-safety-integration.md b/anneal/agent_docs/design/open-questions/rust-safety-integration.md new file mode 100644 index 0000000000..5009d291c4 --- /dev/null +++ b/anneal/agent_docs/design/open-questions/rust-safety-integration.md @@ -0,0 +1,165 @@ + + +# Integration with Rust's safety machinery + +**Status:** Open design discussion. + +Rust has a familiar, compiler-enforced vocabulary for `unsafe fn`, `unsafe` +blocks, and unsafe traits. As of this page's 2026-07-17 review, unsafe fields +were under development upstream; that status is volatile and must be rechecked +before it becomes an implementation premise. Rust also has ecosystem +conventions and lints around `# Safety` documentation and `// SAFETY:` comments. +That machinery tracks only one undifferentiated notion of safety, while Anneal +must support multiple property kinds and stronger proof obligations. V2 must +decide where to extend Rust's system and where to create an Anneal-owned system +alongside it. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-001](../settled-requirements.md#anneal-req-001-v2-is-a-clean-room-redesign), [decision 0001](../decisions/0001-v2-is-a-clean-room-redesign.md) | V1 syntax and its mapping to Rust `unsafe` are evidence, not defaults. | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational) | Soundness remains mandatory under every integration strategy. | +| [ANNEAL-REQ-014](../settled-requirements.md#anneal-req-014-type-invariants-support-arbitrary-property-kinds), [ANNEAL-REQ-015](../settled-requirements.md#anneal-req-015-trait-invariants-support-arbitrary-property-kinds), [decision 0004](../decisions/0004-invariants-support-all-property-kinds.md) | Type and trait invariants are required and must support arbitrary property kinds. | +| [ANNEAL-REQ-016](../settled-requirements.md#anneal-req-016-contracts-distinguish-semantic-roles) | Rust's single safety axis cannot erase distinctions among Anneal obligation roles. | +| [ANNEAL-REQ-022](../settled-requirements.md#anneal-req-022-incremental-adoption-supports-prose), [decision 0005](../decisions/0005-incremental-adoption-supports-prose-justifications.md) | Selected formal obligations may be replaced temporarily by explicit, audited prose justifications. | +| [ANNEAL-REQ-026](../settled-requirements.md#anneal-req-026-upstream-evolution-is-in-scope) | Rust language and specification evolution is in long-term scope. | + +Topic-specific implications: + +- A safe Rust API must remain sound for every type-checked safe use, even when + its implementation uses unsafe code or Anneal tracks additional properties. +- Type invariants cannot be omitted because V1's mechanism was unsound, and V2 + need not wait for unsafe fields: Rust support and Anneal-specific analysis + are both candidates. +- Rust's existing unsafe boundaries offer familiar enforcement and migration + points, while arbitrary property kinds may require Anneal-owned scopes. The + balance between those systems remains the question being decided. + +## The central choice + +At one end of the design space, Anneal could map formal soundness obligations +closely onto Rust's existing unsafe boundaries. This would reuse compiler +checks, programmer expectations, documentation conventions, Clippy lints, and +incremental workflows. A Rust `unsafe` block could be the place where either a +formal proof or an audited prose justification discharges an obligation. + +At the other end, Anneal could maintain a richer parallel system. It could +track separately named property kinds, require proof around operations Rust +does not mark unsafe, and support type invariants before unsafe fields +stabilize. This avoids forcing concepts such as panic freedom or cryptographic +correctness into Rust's single `unsafe` bit. + +A hybrid is plausible: use Rust boundaries as authoritative evidence for some +soundness obligations while layering general property tracking and additional +invariant-sensitive operations on compiler-resolved program facts. The exact +division, reconciliation rules, and user vocabulary remain open. + +## Questions to resolve + +### Which Rust constructs carry Anneal meaning? + +- Does every `unsafe` operation generate an Anneal soundness obligation, or do + obligations attach only to unsafe leaves with modeled semantic guards? +- Is an `unsafe` block evidence of the intended proof scope, a syntactic place + to write a proof, or merely a Rust type-checking construct? +- How are unsafe functions whose callers provide prose `# Safety` contracts + related to machine-readable Anneal contracts? +- Can an operation be safe under Rust's soundness axis but guarded under another + Anneal property kind? If so, what source construct marks it? +- How should unsafe traits and future language features interact with Anneal's + trait invariants? + +Rust's `unsafe` syntax identifies responsibility boundaries; it does not by +itself fully state the semantic preconditions that make an operation sound. +Any design that reuses the syntax still needs an adequate specification of +those preconditions. See [source/model adequacy](source-model-adequacy.md). + +### How are property kinds spelled? + +A hypothetical Rust feature such as `unsafe(soundness)` or +`unsafe(panic_freedom)` illustrates the desired distinction, but does not exist. +V2 must decide whether annotations: + +- name property kinds independently of Rust syntax; +- decorate existing unsafe functions, blocks, traits, and fields; +- introduce Anneal-specific proof scopes for operations that Rust considers + safe; or +- combine these approaches and require exact reconciliation. + +The answer must work for user-defined kinds without requiring a Rust language +change for each new domain. It must also avoid implying that a caller may +violate the soundness of a safe Rust API merely because no Anneal property was +selected. + +### How are type invariants protected? + +V1's `isValid` concept demonstrated the usefulness of type invariants but did +not prevent safe code from mutating fields without re-establishing them. V2 +needs an enforcement boundary. Candidate mechanisms include: + +- Rust unsafe fields, once their exact semantics are usable; +- Anneal analysis that marks reads, writes, borrows, moves, construction, and + destruction of invariant-carrying representation as proof-requiring; +- module or constructor boundaries; +- explicit invariant-opening and invariant-closing operations; +- refinement wrappers whose representation cannot be accessed directly; and +- combinations of these for different kinds of invariant. + +The design must account for pattern matching, field projection, mutable and +shared borrowing, interior mutability, destructuring assignment, unions, +layout operations, drop, and code generated by macros. It must say when an +invariant may be temporarily broken, who owns the capability to restore it, +and how resource-sensitive facts are consumed. See +[contracts and invariants](contracts-and-invariants.md) and +[memory, resources, and effects](memory-resources-and-effects.md). + +### How does prose coexist with proofs? + +Some version of prose-based discharge is required for incremental adoption. +Open choices include: + +- whether an existing `// SAFETY:` comment is enough or must carry an explicit + Anneal marker; +- whether comments discharge individual call-site obligations, whole unsafe + blocks, or selected subtrees; +- which property kinds may use prose; +- whether prose uses an axiom-like or shared admission mechanism, a dedicated + status or provenance record, or another representation, while reports still + distinguish it from axiomatic semantics, incomplete proofs, and checked + evidence; +- whether Anneal checks that every Rust unsafe boundary has either proof or + prose, even when only part of a crate is formally adopted; and +- how later tooling helps replace prose with proofs without changing the Rust + code's structure. + +Prose can mark a trust gap; it cannot silently supply a machine-checked theorem. +The command and ledger semantics are discussed in +[trust and incremental adoption](trust-and-incremental-adoption.md). + +## Evaluation criteria + +Compare candidate integrations by asking: + +1. Does safe Rust retain its unconditional soundness promise? +2. Can the system express independent and dependent property kinds without + abusing Rust's single safety axis? +3. Can every invariant-sensitive operation be found in expanded, + compiler-resolved code, including generated code? +4. Is responsibility visible and familiar enough for Rust engineers to review? +5. Can a project adopt Anneal gradually without disguising trust gaps? +6. Does the design continue to work if Rust gains unsafe fields or richer + safety annotations? +7. Can the implementation fail closed when Rust and Anneal views disagree? + +Useful prototypes should include an invariant-carrying type before unsafe +fields, a crate mixing formal proofs and `// SAFETY:` comments, and a +property other than soundness attached to an operation Rust considers safe. The +compiler metadata needed for those experiments is covered in +[Aeneas and Charon integration](aeneas-charon-integration.md). diff --git a/anneal/agent_docs/design/open-questions/source-model-adequacy.md b/anneal/agent_docs/design/open-questions/source-model-adequacy.md new file mode 100644 index 0000000000..8e907826bd --- /dev/null +++ b/anneal/agent_docs/design/open-questions/source-model-adequacy.md @@ -0,0 +1,168 @@ + + +# Source/model adequacy + +**Status:** Open design discussion. + +Anneal's intended verification pipeline uses Aeneas and Lean to prove that +unsafe operations satisfy their preconditions, yet the correspondence between +Rust and the generated model is only promised for sound Rust programs. An +unsound Rust program may be lowered to a Lean definition that bears no useful +relationship to its source. V2 must close this apparent circularity rather +than merely assume that successful Lean proofs describe the original program. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-005](../settled-requirements.md#anneal-req-005-soundness-is-foundational), [ANNEAL-REQ-006](../settled-requirements.md#anneal-req-006-soundness-specifications-produce-adequate-obligations) | A source-level soundness result requires adequate, non-erasable obligations for all supported Rust safety conditions. | +| [ANNEAL-REQ-007](../settled-requirements.md#anneal-req-007-the-memory-model-is-conservative) | Trusted unsafe-leaf guards must conservatively reflect the normative Rust guarantees being claimed. | +| [ANNEAL-REQ-017](../settled-requirements.md#anneal-req-017-initial-claims-are-artifact-scoped), [decision 0002](../decisions/0002-verification-is-artifact-scoped.md) | The initial theorem concerns one fixed Cargo compilation artifact, not every build configuration. | +| [ANNEAL-REQ-018](../settled-requirements.md#anneal-req-018-generated-rust-is-analyzed-input), [decision 0003](../decisions/0003-expanded-generated-rust-is-input.md) | Expanded generated Rust ingested by Charon is analyzed input rather than trusted merely because a generator produced it. | +| [ANNEAL-REQ-019](../settled-requirements.md#anneal-req-019-coverage-adequacy-is-enforced) | Every potentially invalid source operation in the reported coverage envelope must receive the obligations needed to justify the proof model. | +| [ANNEAL-REQ-020](../settled-requirements.md#anneal-req-020-the-tcb-is-explicit-and-shrinkable), [ANNEAL-REQ-021](../settled-requirements.md#anneal-req-021-results-carry-an-audit-ledger), [decision 0006](../decisions/0006-the-tcb-is-explicit-and-shrinkable.md) | Unproved correspondence, toolchain, coverage, and primitive-semantic assumptions remain explicit and replaceable. | +| [ANNEAL-REQ-026](../settled-requirements.md#anneal-req-026-upstream-evolution-is-in-scope) | Rust, Charon, Aeneas, and Anneal may all change to support a defensible adequacy argument. | + +Topic-specific implications: + +- A Lean theorem about an inadequate or incompletely covered model is not a + theorem about the Rust artifact. Model and tool failures therefore cannot be + reported as successful source verification. +- Proposition-valued function arguments and sidecar call-site theorems are + alternative obligation encodings. Neither is sufficient without complete + coverage and a semantic argument connecting discharged guards to source + validity. +- The exact adequacy theorem, extraction point, coverage unit, and division + between proof and trusted translation remain open. + +## The required semantic connection + +We need a precise theorem connecting source executions, extracted semantics, +and generated proof obligations. Its exact statement is open. Candidate proof +families include: + +- an execution-prefix argument showing correspondence while validity + conditions hold and ruling out a first invalid operation by proving every + required guard; +- a forward or backward simulation maintained under an explicit source + validity invariant; and +- per-artifact translation validation that checks the extracted operations and + obligations against a separately justified semantic relation. + +These are sketches, may overlap, and are neither exhaustive nor accepted. Any +formulation must account for nondeterminism, concurrency, unwind and abort +behavior, infinite executions, provenance, external effects, compiler +transformations, and whatever relation Aeneas actually proves between LLBC and +Lean. + +The important distinction is between the semantic argument and the Lean API +used to present an obligation. Proposition-valued parameters make unguarded +model calls ill-typed; sidecar WP theorems may reuse Aeneas machinery more +directly. Either presentation still requires a theorem explaining why proving +the obligations rules out undefined source behavior. + +## Questions to resolve + +### Where is the authoritative program captured? + +- At which rustc phase must Charon extract the program so operations are still + present and their semantics have not already been changed by optimizations + that assume away undefined behavior? +- Are MIR and LLBC sufficiently expressive to identify every relevant unsafe + primitive and path, including drop glue, compiler-generated shims, intrinsics, + unwinding, and monomorphized calls? +- What compiler transformations occur before extraction, and what assumptions + do they make? +- Which source annotations survive expansion and lowering, and how are they + reconciled with compiler-resolved items? + +[Issue #3041](https://github.com/google/zerocopy/issues/3041) raises the risk +that extraction after UB-exploiting optimization could erase exactly the +operation Anneal needs to guard. This remains an investigation; V2 must not +assume the current extraction point is adequate without evidence. + +### What counts as complete coverage? + +- How are direct calls, trait dispatch, function pointers, closures, virtual + calls, recursion, drop glue, statics, and compiler intrinsics enumerated? +- Is proof coverage stated over syntactic call sites, semantic operations, + reachable monomorphized instances, or another unit? +- How are unreachable code and dead branches justified? +- What happens when Charon or Aeneas omits an unsupported construct? +- How does separate compilation carry verified contracts without assuming that + dependency code was built with different features or targets? +- How does Anneal prove that its annotation index and the LLBC artifact describe + the same items? + +Coverage should be machine-checkable and appear in the audit artifact where it +depends on assumptions. See +[Aeneas and Charon integration](aeneas-charon-integration.md) and +[trust and incremental adoption](trust-and-incremental-adoption.md). + +### What semantics do leaf guards express? + +Raw pointer dereference, pointer arithmetic, reads and writes, allocation, +deallocation, intrinsics, inline assembly, and FFI have different semantic +foundations. For each leaf V2 must determine: + +- the Rust operation being modeled; +- the precondition sufficient to rule out its undefined behaviors; +- the result and effects available to subsequent proofs; +- resource ownership or provenance consumed and produced; +- panic, unwind, abort, and divergence behavior where applicable; and +- which facts are proven, derived from Rust's specification, or trusted. + +An explicit set of assumptions is not automatically a conservative model of +normative Rust guarantees. The relationship must itself be documented and, +where possible, mechanized. Resource-bearing guards are discussed in +[memory, resources, and effects](memory-resources-and-effects.md). + +### What must be proved about the toolchain? + +- Is the adequacy theorem end-to-end, or a composition of rustc-to-LLBC, + LLBC-to-Lean, Anneal instrumentation, Lean kernel, and code-generation claims? +- Which translations are formally verified, validated per artifact, tested, or + trusted? +- Can Anneal independently validate that generated Lean contains all expected + obligations without brittle text rewriting? +- Which host compiler, LLVM, linker, and target hardware assumptions affect the + final claim rather than only tool availability? + +These questions do not require V2 to verify its entire toolchain immediately. +They do require an honest boundary and a path to shrink it. + +## Candidate approaches + +Candidate work can be combined: + +- extend Charon with compiler-resolved annotations and an operation index; +- validate LLBC against an independently generated obligation manifest; +- extend Aeneas's WP semantics with guarded unsafe leaves; +- make guards proposition-valued inputs to selected generated Lean functions; +- generate sidecar theorems and have Anneal verify one theorem per indexed + operation; +- prove an adequacy or trace-simulation theorem connecting complete guards to + source validity; and +- add fail-closed coverage checks for every unsupported or unmatched item. + +Textual patches to generated Lean are less desirable than programmatic +interfaces, but the criterion is robustness and semantic auditability, not a +categorical ban on any implementation technique. + +## Evaluation criteria + +A successful approach must state exactly which source artifact it covers, +identify every operation that can invalidate the source/model relationship, +make missing obligations detectable, preserve outcome and resource semantics, +and expose its trusted assumptions. It should also let V2 reuse Aeneas's WP +machinery rather than rebuilding it without need. + +The result should survive adversarial examples: an invalid operation optimized +away, an unsafe action in generated drop glue, a trait call resolved only after +monomorphization, and a panic path that runs unsafe cleanup. diff --git a/anneal/agent_docs/design/open-questions/trust-and-incremental-adoption.md b/anneal/agent_docs/design/open-questions/trust-and-incremental-adoption.md new file mode 100644 index 0000000000..efbc6d3ed4 --- /dev/null +++ b/anneal/agent_docs/design/open-questions/trust-and-incremental-adoption.md @@ -0,0 +1,163 @@ + + +# Trust and incremental adoption + +**Status:** Open design discussion. + +Anneal must be useful before an entire codebase has been modeled, while making +it impossible to confuse a partially trusted result with an end-to-end proof. +It must also support genuinely external semantics that may remain axiomatic for +the foreseeable future. V2 therefore needs first-class accounting for trust, +incompleteness, and adoption state. + +## Settled constraints + +| Authority | Constraint on this question | +| --- | --- | +| [ANNEAL-REQ-006](../settled-requirements.md#anneal-req-006-soundness-specifications-produce-adequate-obligations) | Non-axiomatic soundness specifications require machine-enforced adequacy rather than human intent alone. | +| [ANNEAL-REQ-017](../settled-requirements.md#anneal-req-017-initial-claims-are-artifact-scoped), [decision 0002](../decisions/0002-verification-is-artifact-scoped.md) | Trust and incompleteness qualify a result about one precisely identified compilation subject. | +| [ANNEAL-REQ-020](../settled-requirements.md#anneal-req-020-the-tcb-is-explicit-and-shrinkable), [decision 0006](../decisions/0006-the-tcb-is-explicit-and-shrinkable.md) | Trusted semantic leaves and the broader end-to-end TCB must be explicit and replaceable by deeper models. | +| [ANNEAL-REQ-021](../settled-requirements.md#anneal-req-021-results-carry-an-audit-ledger) | Every result must expose its exact claim, dependencies, trust, incompleteness, coverage, toolchain, environment, and hardware assumptions. | +| [ANNEAL-REQ-022](../settled-requirements.md#anneal-req-022-incremental-adoption-supports-prose), [decision 0005](../decisions/0005-incremental-adoption-supports-prose-justifications.md) | Selected obligations may temporarily rely on prose, but that reliance is an explicit residual dependency rather than a completed proof. | +| [ANNEAL-REQ-023](../settled-requirements.md#anneal-req-023-axioms-cover-genuine-external-semantics) | Fully adopted code should reserve axioms for genuine semantic boundaries; standard-library primitives and FFI remain important expected uses. | +| [ANNEAL-REQ-024](../settled-requirements.md#anneal-req-024-incompleteness-is-distinguishable-from-external-trust) | An intended but unfinished proof must remain distinguishable from an intentionally axiomatic specification. | + +Topic-specific implications: + +- A result containing residual dependencies must identify their kind, origin, + and affected claim. When a dependency has a known path to stronger evidence, + the ledger should expose it; a successful exit code cannot erase the + dependency. +- The meaning of a user-defined property comes from the user; any unproved + proposition assumed about it remains a residual dependency. Anneal enforces + and reports that assumption but cannot validate the intended meaning. This + differs from responsibility for the adequacy of primitive soundness guards. +- Command statuses, policy profiles, ledger schema, and authorship or + distribution of external specifications remain open. + +## Distinct evidence classifications and roles + +Not every residual dependency is trusted, and not all missing evidence means +the same thing. At minimum, the design must preserve distinctions among: + +- an axiom representing genuinely external semantics; +- a primitive-semantic assumption, with its actual origin and owner; +- a specification whose proof is intended but not complete; +- a call site temporarily justified by a prose `// SAFETY:` explanation; +- source or generated code intentionally outside the adoption scope; +- a construct modeled only through an opaque specification; +- an unsupported, skipped, or unmodeled construct; +- an admitted Lean theorem or equivalent escape hatch; +- a compiler, translator, kernel, runtime, or hardware assumption; and +- a model/tool failure that prevents any defensible claim. + +These may share implementation machinery, but users need to know each item's +status, role, owner, effect on the claim, and any known path to stronger +evidence. An approved semantic assumption may condition a claim; an incomplete +proof remains an unresolved proof obligation; a coverage or tool failure may +instead block the claim. The canonical definitions are in +[result and trust](../result-and-trust.md#what-trust-means). + +## Questions to resolve + +### What does command success mean? + +Candidate policies include: + +- `cargo anneal verify` fails on every incomplete proof but permits explicitly + approved axioms with a ledger; +- a separate incremental profile succeeds with a clearly conditional status; +- one command returns structured assurance grades and uses configurable exit + policy; or +- distinct commands separate end-to-end verification from partial checking. + +The design must avoid a state in which users or CI interpret “success” as a +stronger claim than the artifact supports. Open details include: + +- whether unrequested property kinds appear as gaps; +- whether a deliberately excluded dependency is an error or audited + assumption; +- how policy changes affect reproducibility; +- whether CI can impose a budget or allowlist for trust gaps; and +- what downstream crates may rely on from a partially verified dependency. + +### How are incomplete proofs represented? + +An explicit “specification present, proof incomplete” status may be preferable +to encoding incremental work as an axiom. It is analogous in purpose to Lean's +`sorry`, but V2 need not expose that mechanism directly. + +Questions include: + +- Is incompleteness attached to a theorem, obligation, source region, property + kind, or artifact? +- Does it preserve the intended specification for callers while marking its + proof as incomplete rather than established? +- Can a project prohibit new gaps while grandfathering existing ones? +- Does each gap have an owner, rationale, expiration, or issue link? +- How are transitive gaps summarized without losing their origin? +- Can a proof later replace the gap without changing the public verification + interface? + +### How do prose justifications work? + +Prose support is required, and a prose justification must remain +distinguishable from checked evidence. Its representation and binding semantics +are open: it could be a specialized admitted obligation associated with a Rust +unsafe boundary, a separate evidence status or provenance field, or another +form with Rust-oriented diagnostics. + +We need to decide: + +- which comments Anneal recognizes and how they bind to exact compiler-resolved + operations; +- whether prose is allowed only for soundness or for arbitrary property kinds; +- whether the text is included verbatim or hashed in the ledger; +- whether ordinary Rust linting conventions are reused; +- what happens when code moves and a comment no longer binds unambiguously; and +- how the tool guides conversion from prose to a machine proof. + +This intersects with [Rust safety integration](rust-safety-integration.md). + +### Who authors and distributes external specifications? + +For FFI and platform APIs, the specification might be authored by: + +- each Rust consumer; +- the C, C++, assembly, or platform library author; +- an Anneal standard-library or ecosystem package; or +- a third-party verification authority. + +V2 needs identities, versioning, target constraints, and a way to distinguish a +widely reviewed specification from a local assertion without turning social +trust into a misleading proof claim. Specifications may eventually be backed +by proofs in another system or by a formal ISA model. + +### What exactly is in the ledger? + +The canonical minimum inventory is defined in +[result and trust](../result-and-trust.md#audit-ledger). The remaining questions +concern representation and policy: exact field schema and granularity, stable +identities, normalization and reproducibility, serialization, signing, diff +format, retention and privacy, and the relationship between a machine-readable +artifact and a useful human audit view. + +## Evaluation criteria + +An acceptable design must be fail-closed about unsupported semantics, preserve +the difference between proof and trust, support useful incremental adoption, +and make transitive assumptions visible. It should reward shrinking the TCB, +allow external models to replace axioms, and produce stable artifacts suitable +for code review and CI policy. + +Useful experiments include a crate with one prose-justified call, a dependency +with an incomplete functional proof, an FFI binding with target-specific +axioms, and the same code verified under two compiler or hardware assumptions. +The source coverage needed to populate the ledger is discussed in +[source/model adequacy](source-model-adequacy.md). diff --git a/anneal/agent_docs/design/principles.md b/anneal/agent_docs/design/principles.md new file mode 100644 index 0000000000..b21f97b1a0 --- /dev/null +++ b/anneal/agent_docs/design/principles.md @@ -0,0 +1,144 @@ + + +# Design principles + +This page states Anneal's goals and the choice rules used when +[settled requirements](settled-requirements.md) and +[accepted decisions](decisions/README.md) do not determine an answer. Technical +mechanisms belong in the linked design documents; agent procedure belongs in +[`AGENTS.md`](../../AGENTS.md). + +## Goals and scope + +Anneal's long-term scope includes arbitrarily subtle correctness properties and +arbitrary Rust codebases. That scope guides the architecture; it does not +require the current executable or first milestone to support every Rust +construct or property domain. + +Unsafe Rust leaves soundness obligations which Rust's type system does not +discharge. Giving them rigorous, practical treatment is Anneal's foundational +use case, especially in unsafe-heavy systems code. Anneal must nevertheless +support functional correctness, protocols, panic freedom, resource bounds, and +other user-defined properties in the same framework. + +Anneal is intended for ordinary Rust organizations. Specialists and AI agents +may assist, but Rust engineers must be able to understand, debug, review, and +incrementally adopt the result. + +## Protect soundness and the meaning of every reported claim + +A theorem about modeled behavior supports the corresponding Rust claim only +insofar as the covered Rust behavior remains defined. Correspondence over an +execution prefix may help prove this condition, but soundness is still a +prerequisite for interpreting a model theorem as a fact about the Rust artifact. + +Anneal must account for every operation which can cause undefined behavior +under the supported Rust semantics and generate adequate obligations for it. A +weak, incomplete, or vacuous user specification cannot remove those +obligations. Unsupported semantics, missing coverage, and insufficient evidence +must narrow, condition, or prevent the reported claim instead of disappearing +behind a successful proof check. + +For a user-defined property, Anneal can enforce a precise definition but cannot +infer whether it captures the user's intent. A specification claiming +correspondence with Rust or another external semantics is different: its +adequacy is a claim-relevant dependency which must be justified or reported. +See the [verification model](verification-model.md) and +[result and trust](result-and-trust.md). + +## Prove abstraction boundaries once, then compose them + +An implementation becomes reusable through an abstraction boundary only after +it has been proved to satisfy the declared interface. That interface must +account for every claim-relevant interaction with the context, including +capabilities or resources exchanged across it. For soundness, a reusable safe +API must remain sound under every type-correct safe use admitted by that API +within the stated semantic and compilation envelope. + +Clients may then use the established guarantees without reopening the private +implementation. They may interact through declared mutation, allocation, I/O, +nondeterminism, or other effects, but neither side may impose undeclared +requirements on the other. This interface-relative isolation—not absence of +interaction—is the locality Anneal seeks. See +[contextual refinement](verification-model.md#contextual-refinement). + +## Introduce only the semantic machinery the claim requires + +A pure value-level contract is preferred when it fully describes the +abstraction boundary. Resource, provenance, initialization, ownership, +concurrency, protocol, or effect semantics are required whenever ignoring them +could invalidate the claim. + +For example, a freely reusable Lean fact cannot by itself authorize exclusive +mutation: two consumers could each cite it to justify access. Whether enforced +by a resource proposition, a state- or world-indexed weakest precondition, a +monadic discipline, or another mechanism, the proof interface must retain the +permission's usage rules. + +This yields a hybrid model without making “hybrid” a goal. The boundary between +functional translation and richer semantics evolves with Aeneas and Charon. +Revision-sensitive facts belong in the +[Aeneas and Charon reference](../reference/aeneas-and-charon.md); unresolved +architecture belongs in +[memory, resources, and effects](open-questions/memory-resources-and-effects.md). + +## Reuse general proof machinery after deriving the right Rust obligation + +Rust semantics determine the obligations. Once an obligation becomes a general +proof problem, Anneal favors proof abstractions maintained by Lean and +Aeneas—and compiler-resolved interfaces maintained by Charon—over parallel +special-purpose mechanisms. + +For example, `index < slice.len()` is one arithmetic sub-obligation among the +guards for `slice.get_unchecked(index)`. Aeneas's weakest-precondition +machinery and Lean's arithmetic support can derive that inequality from a +preceding bounds check; a separate Anneal bounds logic would duplicate rather +than improve the semantics. Other unsafe operations may additionally require +provenance, liveness, initialization, authority, or similar conditions which +need richer machinery; a concrete mismatch of that kind justifies extending +the underlying abstraction. + +This example does not decide how obligations are encoded. Interface and +upstreaming choices remain in the +[Aeneas and Charon integration discussion](open-questions/aeneas-charon-integration.md). + +## Expose and reduce every trusted dependency + +A dependency is trusted for a claim when the claim relies on its correctness +but the included checked evidence does not establish it at the claimed semantic +endpoint. Translation into Lean does not itself remove trust. + +Semantic assumptions, extraction and correspondence, tool correctness, +pipeline integration, and execution-platform assumptions play different roles +and must remain distinguishable. An incomplete proof is an unresolved +obligation, not an approved semantic boundary; coverage gaps and tool failures +may narrow or block a claim rather than become assumptions. + +Trusted dependencies must be visible and replaceable by stronger evidence. +Moving one into a helper or upstream component does not reduce trust unless the +end-to-end dependency is removed. Definitions, classifications, and audit +requirements live in [result and trust](result-and-trust.md). + +## Make partial adoption useful without calling it complete + +Anneal must support incremental adoption, including selected prose +`// SAFETY:` justifications and a distinct representation of unfinished +proofs. Neither may silently become checked evidence. Results must identify what +was checked, what remains, which claim the evidence supports, and what would +strengthen it. + +Among designs preserving those distinctions, this principle favors stable +proof interfaces, source-linked diagnostics, resilience to small changes, and +feedback useful to ordinary Rust engineers. + +## Relationship among the principles + +Soundness and claim integrity constrain acceptable designs. Among those +designs, simplicity, reuse, trust reduction, coverage, maintenance, and user +experience require case-specific judgment rather than a permanent total order. diff --git a/anneal/agent_docs/design/result-and-trust.md b/anneal/agent_docs/design/result-and-trust.md new file mode 100644 index 0000000000..5b62158340 --- /dev/null +++ b/anneal/agent_docs/design/result-and-trust.md @@ -0,0 +1,374 @@ + + +# Result and trust + +This document defines what identifies an Anneal result, which dimensions its +claim must state, how checked evidence differs from residual dependencies, and +what users must be able to audit. The +[verification model](verification-model.md) explains how local obligations +compose to produce the result. + +Anneal does not eliminate trust by translating Rust into Lean. It must instead +report exactly which claim its evidence supports and expose every dependency +needed to connect that evidence to the claim. The exact serialization, command +profiles, and exit-status policy remain open; see +[trust and incremental adoption](open-questions/trust-and-incremental-adoption.md). + +## What trust means + +A dependency is trusted for a reported claim when that claim relies on the +dependency's correctness but the result's included checked evidence does not +establish it at the claimed semantic endpoint. Trust is therefore relative to +a particular result and claim, not an intrinsic label on a component. A +compiler may be irrelevant to a theorem stated only about a Lean model but +essential to a claim about the binary it produces. + +Different trusted dependencies play different roles. A semantic assumption +says what an operation or environment means. Tool trust says that a component +handled its inputs and semantics correctly. Integration or correspondence +trust says that the components, identities, and artifacts are connected to the +same compilation subject correctly. Execution-substrate trust connects a Rust +or binary claim to the platform and hardware on which it runs. + +An incomplete proof and an unchecked admission have distinct statuses, but +neither includes checked evidence for the required argument. An incomplete +proof records unresolved proof work; an unchecked admission is an escape hatch. +Neither becomes an intentional semantic boundary merely because Lean can +represent both using axiom-like declarations. Likewise, a coverage gap or tool +failure may narrow or block a claim instead of becoming an assumption the claim +is permitted to rely on. **Residual dependency** is therefore broader than +**trusted dependency**. + +## Compilation-subject and result identity + +Anneal's initial subject is one concrete Cargo compilation artifact. Here, +“compilation artifact” means the compiler-resolved Rust program and semantic +configuration selected for verification, not the native executable, library +archive, or other file emitted by Cargo. “Compilation subject” is the preferred +phrase when that distinction matters. + +The compilation subject changes whenever an input can change the Rust program +presented to Charon or its source-level semantics. Rust emitted by procedural +macros or build machinery and then ingested by Charon is part of that subject. +It is analyzed like checked-in Rust rather than trusted merely because a +generator produced it. This does not make execution of the generator itself +part of the proved Rust program, nor does it verify every output that the +generator could produce. + +A verification result has a separate identity. It combines the compilation +subject with a precise claim, checked evidence, residual dependencies, and the +models and tools that produced or checked them. Changing a proof, property +selection, translator, semantics, or trusted specification can therefore +produce a different result about the same compilation subject. + +Classify an input by what it can change: + +- an input that changes the compiler-resolved Rust program or its source + semantics participates in compilation-subject identity; +- an input that changes extraction, modeling, obligations, evidence, selected + claim, or assumptions participates in verification-result identity; and +- an input that changes only the relationship between the Rust subject and a + binary execution qualifies that execution claim. + +One component may have several roles. A rustc revision, for example, can +change the compilation subject and also remain part of the end-to-end TCB. +Classify the actual dependency rather than permanently assigning each tool to +one bucket. + +Verification across targets, features, panic strategies, dependency versions, +or other build-matrix cells initially produces multiple subject-specific +results. Tooling may group and deduplicate them, but must identify which cells +were checked, omitted, or assumed. A prior result must not be silently +generalized to a related subject. + +## Claim dimensions + +“Verified” is incomplete unless the result states independent dimensions of +the claim: + +### Property and guarantee + +The result identifies each asserted property, the guarantee established for +it, and every dependency on another property or assumption. Rust soundness is +foundational; selecting another property does not silently remove the +soundness basis needed to interpret the model as Rust. + +### Behavior + +The result identifies which source behaviors the guarantee covers. Normal +return, panic and unwind, abort, and divergence can support different +obligations. A soundness result does not imply panic freedom or termination +unless those guarantees are also stated and proved. + +### Client and coverage envelope + +The result identifies the items, paths, call sites, generic instances, and +clients covered. Proving all concrete uses in one compilation subject is +different from proving contextual refinement for every type-correct safe use +admitted by an API within a stated envelope. Omitted or unsupported coverage +may not be inferred to have been checked. + +### Semantic endpoint + +The result identifies the semantic object about which it makes a claim. A +Lean-kernel theorem concerns declarations in a Lean environment. A claim about +the Rust compilation subject additionally depends on adequate extraction, +translation, obligation generation, and Rust semantics. A claim about a +compiled binary executing on target hardware additionally depends on the +compiler, linker, ABI, platform, and hardware connection. + +These endpoints and the other dimensions are not one linear hierarchy. A +result can strengthen its client quantification without extending to target +hardware, or add panic freedom without changing its semantic endpoint. Every +reported result must state the actual combination rather than present one +ambiguous assurance grade. + +### Conditions + +The claim is relative to every explicit semantic, environmental, and trusted +dependency that remains after proof checking. A condition can make a result +useful without making it unconditional. Its type and consequences must remain +visible. + +## Evidence and residual dependencies + +Every evidence-graph leaf, proof obligation, and coverage boundary needs enough +classification for users and tools to distinguish its evidence, its role in +the claim, and its coverage or modeling disposition. These dimensions are +independent even if the eventual report schema represents them differently. + +### Evidence classification + +The following distinctions must remain observable. They need not become +mutually exclusive values in one status enum: the eventual schema may use +statuses, subtypes, provenance fields, or several of these. + +- **Checked evidence:** Lean or another accepted checker established the + obligation relative to that checker's environment and assumptions. +- **Approved assumption:** an explicit premise is permitted to condition the + reported claim without evidence establishing it in this result. Its role, + origin, owner, and effect on the claim must be recorded. A specialized form, + such as a prose justification, retains that more specific provenance. +- **Incomplete proof:** a formal obligation is intentionally recorded as work + whose checked evidence has not yet been completed. +- **Unchecked admission or escape hatch:** an admitted theorem, unclassified + axiom, or equivalent bypass supplies no ordinary checked evidence. It must be + detected and reported separately from intentional incompleteness and approved + semantic boundaries. +- **Prose justification:** a human safety argument is relied upon for + incremental adoption in place of a machine-checked proof. Whether the schema + represents it as a specialized admission, a distinct status, or another form + remains open, but the result must preserve the distinction. +- **Tool or model failure:** verification could not establish the requested + result. This is not a source-program outcome and supplies no evidence that + the source property holds or fails. + +### Coverage and modeling disposition + +- **Body or path selected for analysis:** the named implementation body or path + participates in the evidence graph. Its operations still require supported + semantics and adequate obligations. +- **Specification-only or opaque body:** clients use a specification without + analyzing the implementation body at this endpoint. This can be a legitimate + trusted semantic leaf rather than a coverage gap; the specification still + needs its own evidence classification and role in the claim. +- **Outside the selected adoption or coverage scope:** a named item, path, or + generated input is deliberately excluded from the claimed envelope. +- **In scope but uncovered or unreconciled:** an item, path, call, or operation + belongs to the claimed envelope but is absent from or not connected to the + evidence graph despite having supported semantics. This is a coverage + adequacy failure, not an intentional scope boundary. +- **Semantics represented:** the checked model assigns semantics and generates + obligations for the operations relevant to the claim. Whether that + representation and those obligations are adequate is classified separately + as a claim-relevant dependency. +- **Unsupported or unmodeled:** a relevant construct or semantics is not + represented by the checked model. The result must identify the claim this + prevents, narrows, or conditions. + +Coverage and modeling are themselves distinct: selecting a body does not prove +that every operation in it is modeled. A result may therefore need more than +one of these classifications. + +### Role in the claim + +- **Program-proof obligation:** the result must establish a primitive guard, + callee precondition, invariant, contract guarantee, or property-dependency + edge for the analyzed program. Incompleteness, prose, or an admission changes + its evidence treatment, not this role. +- **Program-semantic dependency:** the result relies on the specified meaning + of a primitive Rust or standard-library operation, FFI, assembly, an ISA, a + platform interface, or another part of the modeled program. Its origin and + owner must be recorded. Anneal is responsible for the adequacy of + specifications it provides and for exposing the adequacy dependency of any + specification it imports. +- **User-property dependency:** a user-authored proposition is used without + proof. Merely defining the intended meaning of a user property is part of the + claim, not a residual dependency; assuming that the program satisfies it is. + Anneal cannot infer whether the definition captures the user's intent. +- **Correspondence or integration dependency:** the result relies on source + extraction, translation, obligation coverage, identity reconciliation, or + composition connecting the same compilation subject correctly across stages. +- **Tool-implementation dependency:** the result relies on Anneal, Charon, + Aeneas, Lean, rustc, LLVM, a linker, or another tool behaving correctly. +- **Execution-substrate dependency:** the result relies on an ABI, allocator, + operating system, firmware, external service, foreign library, hardware + behavior, or another condition not established by the program proof. + +The final names and machine representation are open. Their semantic +distinctions are not. In particular, an approved semantic assumption, an +unfinished proof, an unchecked admission, a prose argument, an opaque body, a +coverage gap, and a tool failure support different conclusions. One item can +carry classifications in several dimensions, and its role alone does not +determine whether it allows, conditions, narrows, or blocks a result. + +An undischarged obligation means that Anneal has not established the requested +claim. It is a useful diagnostic about missing evidence, not by itself a proof +that the Rust source violates the property. + +## Two trust boundaries + +Evidence classification and role do not replace the need to distinguish the +scope of a trust boundary. Anneal must distinguish: + +- the **trusted semantic leaf boundary**: program operations whose behavior or + soundness requirements are specified axiomatically instead of proved from a + deeper model; and +- the **end-to-end TCB**: every implementation and assumption needed to connect + checked evidence to the claimed Rust or target execution. + +The initial semantic leaf boundary may include raw-pointer operations, unsafe +standard-library functions, intrinsics, assembly, FFI, and platform operations +whose behavior is exposed through axiomatic specifications rather than derived +from a deeper implementation model. Anneal's standard library will likely use +the same axiom facility to specify some of these leaves. Anneal's authors are +responsible for the adequacy of Anneal-provided soundness specifications. + +The end-to-end TCB is much broader. Depending on the semantic endpoint, it can +include Anneal's obligation generation, Charon's extraction, Aeneas's +translation and semantics, Lean's kernel and proof environment, rustc, LLVM, +linking, the interpretation of Rust and target specifications, operating +systems or firmware, foreign libraries, and host and target hardware. + +A small program-semantic leaf boundary does not make this broader TCB small. +The audit ledger must make clear which boundary a change actually shrinks. + +## Audit ledger + +Every result must expose enough information to reproduce its subject, interpret +its claim, inspect its evidence, and audit its residual dependencies. At +minimum, the ledger records: + +### Claim and scope + +- the property guarantees asserted and their dependencies; +- covered behaviors and exceptional outcomes; +- the client, item, path, call-site, generic-instance, and other coverage + boundaries; and +- the semantic endpoint and every condition needed to reach it. + +### Evidence and gaps + +- each obligation and dependency, with its evidence classification, role, and + any applicable coverage or modeling disposition; +- every trusted semantic leaf and axiom, including origin, owner, and affected + properties; +- every incomplete or admitted proof and every prose justification, with a + source location where applicable; +- every specification-only or opaque body, with the corresponding + specification and evidence classification; +- every skipped, unsupported, or unmodeled item or operation; +- coverage gaps and the claims they prevent or condition; and +- dependencies among proofs, properties, specifications, and assumptions. + +### Compilation subject + +- workspace, package, Cargo target, target kind, profile, source revision or + other source identity; +- dependency resolution and enabled features; +- target triple or specification, `cfg` values, panic strategy, overflow + behavior, and other source-semantics-relevant compiler options; +- generated Rust, proc-macro expansion, build outputs, and included files that + form the compiler-resolved subject; and +- relevant environment variables, build-script directives, ABI, and other + inputs or assumptions affecting that subject. + +### Verification evidence and toolchain + +- Anneal, Aeneas, and Charon versions or revisions, options, models, + obligations, and downstream semantic patches; +- rustc, the Rust standard library, LLVM, linking tools, and relevant compiler + options; +- the LLBC, Lean declarations, checked proof artifacts, Lean, Lake, Mathlib, + and other proof-library versions needed to identify or reproduce the + evidence; and +- proof, extraction, translation, and reporting configuration not already + captured by the compilation subject. + +### Execution substrate + +- operating-system, firmware, external-service, foreign-library, and platform + assumptions relevant to the claim; +- the host hardware or trusted execution environment on which verification ran + to the degree needed to reproduce or assess the result; and +- the target hardware model or concrete implementation assumed by any binary + execution claim. + +If a result stops at a model or Rust-subject claim, the ledger states that +binary and target-hardware execution are outside the claim rather than implying +they were verified. Host hardware running the checker may nevertheless remain +in the practical TCB. + +Recording a field does not necessarily make it part of a future canonical +content identifier. Defining normalization, semantic equivalence, provenance, +signatures, storage formats, and the useful granularity of hardware identity +remains open. The ledger may not omit a claim-relevant dependency merely +because its canonical encoding is unsettled. + +## Fail-closed reporting + +“Fail closed” means Anneal must never silently report a claim stronger than its +evidence supports. It does not predetermine one command name or exit-code +policy. + +An approved external axiom may be compatible with a successful result whose +claim is explicitly relative to that axiom. An explicitly named incremental +mode may report a weaker conditional result with incomplete proofs or prose +justifications. Whatever policy is chosen: + +- every successful exit has a documented meaning; +- conditional or incomplete evidence is not labeled as an unconditional + verification result; +- omitted coverage remains visible and qualifies the claim; +- property dependencies cannot be disabled without being discharged or + reported as conditions; +- model and tool failures are not treated as source behaviors; and +- users can compare results and ledgers as evidence or trust changes. + +The distinction between a strictly verified mode and conditionally checked +profiles remains open. Anneal must settle that user-facing policy explicitly +rather than allowing implementation accidents to define it. + +## Reducing trust over time + +Stable abstraction contracts should be separable from the current depth of +their implementation model. This permits, for example: + +- a primitive-operation axiom to be replaced by a proved Rust operational + model; +- an assembly axiom to be replaced by an ISA-level proof; +- an FFI specification to be connected to a verified foreign implementation; +- a compiler assumption to be replaced by translation validation or verified + compilation; or +- a hardware assumption to be connected to a formal hardware model. + +The replacement reduces trust only if it supports the same or a stronger +end-to-end claim and removes the old dependency from the ledger. Moving an +assumption into generated code, a helper whose body is not modeled, or another +project without proving it does not shrink the TCB. diff --git a/anneal/agent_docs/design/settled-requirements.md b/anneal/agent_docs/design/settled-requirements.md new file mode 100644 index 0000000000..f09e9edc1c --- /dev/null +++ b/anneal/agent_docs/design/settled-requirements.md @@ -0,0 +1,274 @@ + + +# Settled requirements + +These requirements record constraints that have been unambiguously accepted +for Anneal V2. They deliberately avoid choosing among implementations still +under discussion. Stable identifiers allow code, decisions, and open questions +to refer to the requirement they serve. They are an atomic registry, not a +second explanation of the design philosophy: use the +[design principles](principles.md) to understand why these constraints matter +and the linked design documents for their canonical elaboration. + +## Project scope + +### ANNEAL-REQ-001: V2 is a clean-room redesign + +V2 must be designed from its goals and current evidence rather than inheriting +V1 by default. V1 code and ideas may be reused deliberately. Their existence is +not evidence that V2 should preserve them. + +See [decision 0001](decisions/0001-v2-is-a-clean-room-redesign.md). + +### ANNEAL-REQ-002: General properties + +The long-term architecture must support arbitrarily complex, user-defined +correctness properties. It must not encode an assumption that soundness is the +only property worth verifying. + +### ANNEAL-REQ-003: General Rust use cases + +The long-term architecture must be capable of covering arbitrary Rust +codebases and use cases. Initial milestones may support a strict subset, but +the architecture must not require unsafe-heavy domains to abandon their +essential memory, concurrency, or external-effect semantics. + +### ANNEAL-REQ-004: Extensibility before breadth + +Initial V2 need not ship specialized backends for deadlock freedom, +hyperproperties, cryptographic correctness, quantitative bounds, +probabilistic properties, or every other anticipated domain. It must leave a +path to add such domains without redesigning the core composition model. + +## Soundness and semantic fidelity + +### ANNEAL-REQ-005: Soundness is foundational + +Anneal must treat Rust soundness as a non-optional foundation of a faithful +verification result. Selecting another property kind must not silently disable +the soundness assumptions on which source-to-model correspondence depends. + +### ANNEAL-REQ-006: Soundness specifications produce adequate obligations + +For every non-axiomatic source of Rust soundness requirements, Anneal must +derive obligations sufficient for the supported semantics. In particular, the +specification of a primitive operation must impose the actual conditions +needed for its sound use. A weak, incomplete, or vacuous user contract must not +be able to erase those conditions. + +This is **obligation adequacy**: it concerns whether the generated obligation +is the right one. The separate coverage requirement +[ANNEAL-REQ-019](#anneal-req-019-coverage-adequacy-is-enforced) concerns +whether every relevant operation actually receives and discharges such an +obligation. How Anneal establishes either property is open; see +[source/model adequacy](open-questions/source-model-adequacy.md). + +### ANNEAL-REQ-007: The memory model is conservative + +Any Anneal-owned abstraction of Rust memory and unsafe operations must be a +conservative formalization of the normative guarantees Anneal claims to +support, not merely an undocumented set of convenient assumptions. Ambiguous +prose in Rust's specifications must be surfaced, resolved with the relevant +Rust teams where possible, and recorded as an assumption until resolved. + +### ANNEAL-REQ-008: Resource semantics are preserved + +Lifting separation-logic assertions, ownership, provenance, initialization, or +protocol state into Lean must preserve their usage discipline. Such resources +must not become freely reusable ordinary facts when that would invalidate the +reported claim. In particular, simplifying their use may not compromise +soundness. + +## Local and global verification + +### ANNEAL-REQ-009: Local contract obligations + +Locally, verification must establish that an item's preconditions imply its +applicable guarantees and that every invocation satisfies the required +preconditions or properties of its callees. + +The exact treatment of normal return, panic, unwind, abort, and divergence is +open; this requirement does not imply that every verified item terminates +normally. + +### ANNEAL-REQ-010: Local results compose globally + +Local obligations must compose into a whole-artifact guarantee relative to an +explicit set of trusted leaves and environmental assumptions. A caller must not +need to re-verify the private body of a callee whose contract has been +established. + +### ANNEAL-REQ-011: Long-running and exceptional behavior + +The verification model must be able to express and justify: + +- a server that executes without bound while preserving invariants; +- code that remains sound while panicking; +- unwind cleanup relevant to soundness; and +- code that catches a panic and continues execution. + +Anneal must not equate successful verification with normal termination in all +cases. + +### ANNEAL-REQ-012: Property dependencies + +Property kinds may depend on one another. All supported properties ultimately +depend on soundness, and a soundness obligation may itself rely on a declared +guarantee of another property kind. For example, a callee's functional +guarantee that an index is in bounds may discharge a caller's raw-pointer +soundness obligation. The architecture must not isolate each property kind in +a universe that cannot express these dependencies. + +“Ultimately depend on soundness” describes the semantic basis needed to +interpret model theorems as claims about Rust; it does not impose an acyclic +proof order in which soundness is always established first. Mutually dependent +obligations must be discharged jointly or by another sound treatment of +cycles. The representation and proof mechanism remain open. + +### ANNEAL-REQ-013: Property selection + +Users must eventually be able to choose which non-foundational property kinds +are enforced by a `cargo anneal verify` invocation. Dependency closure, +reporting, command modes, and handling of excluded dependencies remain open. + +## Contracts and invariants + +### ANNEAL-REQ-014: Type invariants support arbitrary property kinds + +V2 must support invariants associated with types, and those invariants must not +be limited to soundness. The V1 `isValid` mechanism is not an acceptable +implementation because safe field mutation could bypass invariant +re-establishment. + +V2 may build on Rust unsafe fields, perform its own field-access and mutation +analysis, or use another sound mechanism. It need not wait for unsafe fields to +stabilize. + +### ANNEAL-REQ-015: Trait invariants support arbitrary property kinds + +V2 must support invariants associated with traits for arbitrary property +kinds. It must enforce the invariant at the implementation site and make the +established invariant available where the corresponding trait bound is known. + +The V1 spelling `isSafe` is not a commitment to syntax or to a soundness-only +meaning. + +### ANNEAL-REQ-016: Contracts distinguish semantic roles + +The architecture must be capable of distinguishing a caller obligation needed +for Rust soundness from an ordinary functional-domain precondition and from +obligations of other property kinds. Rust's single `unsafe` axis does not erase +these semantic differences, even if V2 initially maps several of them onto +existing Rust syntax. + +## Artifact and translation boundary + +### ANNEAL-REQ-017: Initial claims are artifact-scoped + +The initial unit of verification is one Cargo compilation artifact with fixed +target, features, `cfg` values, dependencies, panic strategy, generated code, +and relevant environment. A claim across a build matrix requires multiple +artifact claims or future quantified support. + +See [decision 0002](decisions/0002-verification-is-artifact-scoped.md). +The subject and result identities are elaborated in +[result and trust](result-and-trust.md). + +### ANNEAL-REQ-018: Generated Rust is analyzed input + +Rust code produced by proc macros and build machinery and subsequently ingested +by Charon must be treated as part of the artifact being analyzed, rather than +trusted merely because a generator produced it. This does not by itself settle +how to model every non-Rust effect of a build script. + +See [decision 0003](decisions/0003-expanded-generated-rust-is-input.md). + +### ANNEAL-REQ-019: Coverage adequacy is enforced + +Anneal must ensure that every potentially invalid source operation in the +reported coverage envelope is guarded by the obligations needed to justify +the model used for its proof. An operation, path, or relevant generated item +must not disappear from coverage merely because the obligation generator, +translator, or proof interface failed to represent it. + +This is **coverage adequacy**: it concerns complete application of obligations +whose semantic content is governed by +[ANNEAL-REQ-006](#anneal-req-006-soundness-specifications-produce-adequate-obligations). +The encoding and enforcement mechanism remain open; see +[source/model adequacy](open-questions/source-model-adequacy.md). + +## Trust and adoption + +### ANNEAL-REQ-020: The TCB is explicit and shrinkable + +V2 may rely on a small set of trusted leaves, but they must be explicit, +auditable, and replaceable by deeper models over time. Near-term examples may +include unsafe standard-library leaves, intrinsics, raw-pointer operations, +FFI, and assembly. + +See [decision 0006](decisions/0006-the-tcb-is-explicit-and-shrinkable.md). +The program-semantic leaf boundary and the broader end-to-end TCB are +distinguished in [result and trust](result-and-trust.md). + +### ANNEAL-REQ-021: Results carry an audit ledger + +Users must be able to determine what remains trusted or incomplete. The ledger +must identify the exact subject and claim, checked evidence, residual +dependencies, coverage limits, relevant toolchain, and host and target +assumptions. The canonical minimum inventory is maintained in +[result and trust](result-and-trust.md#audit-ledger); the exact schema and +presentation remain open. + +### ANNEAL-REQ-022: Incremental adoption supports prose + +Some form of existing prose safety justification must be able to stand in for +selected Anneal proofs during incremental adoption. Such a justification is +not a machine-checked proof and must be identifiable in the audit ledger. + +See [decision 0005](decisions/0005-incremental-adoption-supports-prose-justifications.md). +Its evidence classification is defined in +[result and trust](result-and-trust.md#evidence-and-residual-dependencies). + +### ANNEAL-REQ-023: Axioms cover genuine external semantics + +In a fully adopted codebase, axioms should be reserved for genuine semantic +boundaries. Anneal's own standard library will likely use the same facility to +specify primitive unsafe operations, and FFI will likely require user- or +library-authored axioms for the foreseeable future. Who should author and +distribute FFI specifications remains open. + +### ANNEAL-REQ-024: Incompleteness is distinguishable from external trust + +The design must be able to report a proof that is not yet completed separately +from a specification intentionally taken as axiomatic. It is open whether this +uses a first-class incomplete-proof mechanism, command profiles, Lean `sorry`, +or another representation. + +## Ecosystem and usability + +### ANNEAL-REQ-025: Existing proof machinery is preferred + +V2 should build on suitable abstractions maintained by Lean, Aeneas, and their +standard libraries, including WP specifications and tactics, unless a concrete +benefit justifies replacement. This is a strong engineering preference rather +than a prohibition on new machinery. + +### ANNEAL-REQ-026: Upstream evolution is in scope + +Changes or additions to Aeneas and Charon are in scope. In the longer term, +Rust language and specification changes are also in scope. Short-term +implementation constraints must not be documented as permanent project +philosophy. + +### ANNEAL-REQ-027: Ordinary Rust engineers are a target audience + +The eventual workflow must be usable in normal Rust organizations, including +by engineers without formal-methods specialization. Human and AI assistance, +diagnostics, stable proof interfaces, and gradual adoption may all contribute; +none may weaken the meaning or auditability of a successful result. diff --git a/anneal/agent_docs/design/verification-model.md b/anneal/agent_docs/design/verification-model.md new file mode 100644 index 0000000000..44bfdffb5a --- /dev/null +++ b/anneal/agent_docs/design/verification-model.md @@ -0,0 +1,239 @@ + + +# Verification model + +This document describes how Anneal derives a verification result. It does not +choose an annotation syntax, outcome taxonomy, Lean encoding, command mode, or +report format. Subject and result identity, evidence classifications, trust +boundaries, and the canonical audit-ledger contents are defined in +[result and trust](result-and-trust.md). + +The high-level derivation is: + +```text +identified Rust subject ++ requested claim dimensions ++ evaluated evidence graph with classified leaves += reported result stating the established claim and remaining gaps +``` + +Each term matters. Evidence about an unidentified program is not reproducible. +A theorem without a precise requested claim invites overinterpretation. Local +proofs without an evaluated evidence graph do not establish a global result. +Each leaf must be classified as checked evidence, an admissible assumption, a +coverage limit, or a blocking gap or failure; otherwise an axiom, omitted +operation, or unfinished proof disappears into hidden trust. The reported +result states which claim was actually established, any explicit conditions +on it, and why each residual dependency remains. + +The [worked byte-buffer example](worked-example.md) illustrates this model +without ratifying a concrete proof architecture. + +## Subject and claim + +Anneal initially verifies one concrete Cargo compilation subject. Generated +Rust ingested by Charon is part of that subject rather than trusted because a +proc macro or build process produced it. The exact target, features, `cfg` +values, dependencies, panic strategy, generated inputs, and relevant +environment delimit the program to which the result applies. + +A claim about that subject has several independent dimensions: + +- the properties and guarantees asserted, including their dependencies; +- the source behaviors to which those guarantees apply, such as normal return, + panic and unwind, abort, or divergence; +- the client and coverage envelope, from concrete calls in one artifact to + every type-correct safe use admitted by an API within a stated envelope; and +- the semantic endpoint, from a theorem about a Lean model through a claim + about the Rust artifact to execution of a compiled binary on target + hardware; and +- the explicit conditions on which the claim depends. + +These dimensions must not be collapsed into one ladder of “verification +levels.” A source-level soundness result need not establish panic freedom. A +whole-artifact proof of concrete calls need not justify every separately +compiled client. A theorem checked by Lean need not establish a hardware +execution claim without the correspondence and toolchain dependencies needed +to connect them. + +The reporting definition and identity of each dimension are maintained in +[result and trust](result-and-trust.md#claim-dimensions). This document +describes the proof structure from which they are derived. + +## Local obligations + +For an item `f` and a selected property `P`, the schematic local claim is: + +1. assume `f`'s applicable preconditions, invariants, capabilities, + environmental conditions, and already established interface guarantees; +2. show that every call and primitive operation made by `f` satisfies the + required preconditions and property dependencies of the invoked operation; + and +3. show that every behavior covered by the claim establishes the applicable + guarantee of `f`'s contract. + +For a normal-return functional contract, this specializes to the familiar +statement that preconditions imply postconditions. It does not imply that all +claims require normal termination. A soundness claim may permit divergence or +a safe panic while requiring every executed prefix and relevant unwind cleanup +to remain sound. + +The same shape applies when an interface carries resources or effects, but its +assumptions and guarantees are not necessarily freely reusable propositions. +Ownership, provenance, initialization, permissions, protocol state, or an +opened invariant may need to be consumed, transferred, framed, or +re-established. The local proof interface must retain those rules. Treating a +resource as an ordinary duplicable Lean fact would change the claim rather than +simplify its proof. + +Type and trait invariants participate in these local interfaces. A type +invariant must be established and preserved at every relevant operation; a +trait invariant must be established by an implementation and made available +where its trait bound is known. Their concrete enforcement and syntax remain +open in [contracts and invariants](open-questions/contracts-and-invariants.md). + +## Global closure + +Local results form an evidence graph: + +- nodes establish item contracts, invariants, primitive specifications, or + deeper semantic facts; +- call edges require callers to establish callees' preconditions; +- property-dependency edges allow one guarantee to discharge an obligation of + another property; and +- leaf edges end either in checked evidence or in an explicitly classified + residual dependency. + +For example, a callee's functional guarantee that an index is below a buffer +length may discharge the soundness precondition of a caller's raw-pointer +access. This does not make soundness optional; the functional theorem is an +edge in the proof that the pointer access remains sound. + +An artifact-level claim follows only when every relevant non-leaf node +satisfies its local contract, every required edge is discharged, coverage is +adequate, and each remaining assumption is admissible for and included in the +conditions of that claim. Mutually dependent properties may require joint +reasoning; the graph model does not impose an artificial proof order in which +every soundness theorem must be completed before any other property can +contribute to it. + +For Rust soundness, the conditions assigned to primitive unsafe leaves must be +adequate. Anneal is responsible for conditions it provides and must report the +adequacy dependency of any specification it imports. If the conditions are +sufficient for the supported Rust semantics and every use establishes them, +the local results compose into an artifact-level soundness claim relative to +the recorded semantic and environmental dependencies. + +Classification alone does not discharge a residual dependency. Its status +determines whether Anneal can establish the requested claim relative to an +admissible assumption, must narrow or condition the claim, or cannot establish +a substantive claim at all. A tool failure supplies no evidence, and some +coverage gaps prevent rather than merely qualify a claim. Command policy may +decide which established conditional results count as success; it may not turn +a missing evidentiary connection into an assumption. See [evidence and residual +dependencies](result-and-trust.md#evidence-and-residual-dependencies). + +## Adequacy closes the source/model loop + +Anneal intends to use a model that is promised to correspond to sound Rust in +order to prove that the Rust subject is sound. It cannot resolve this apparent +cycle by assuming soundness unchecked. + +A source-level soundness result therefore needs both complete, adequate guards +for potentially invalid source operations and a justified correspondence from +the guarded source execution to the proof model. It must not assume the very +whole-program soundness that the guards are intended to establish. The exact +correspondence theorem and proof decomposition remain open. + +One candidate is a guarded-prefix argument: establish correspondence before a +first invalid source operation, identify and guard every operation that could +be that first invalid operation, and use checked evidence for those guards to +rule such an operation out. A trace simulation, translation validation, or +another construction may establish the same required connection instead. See +[source/model adequacy](open-questions/source-model-adequacy.md). + +Whichever proof family is chosen, two different adequacy requirements are +involved: + +- **Obligation adequacy** means that each generated guard expresses the right + Rust validity conditions. Primitive semantics and other non-axiomatic + sources of Rust requirements must determine those conditions; a user + contract cannot weaken them away (ANNEAL-REQ-006 in the + [settled requirements](settled-requirements.md)). +- **Coverage adequacy** means that every potentially invalid operation in + scope actually receives such a guard and that missing operations, paths, or + generated items prevent an unconditional result + ([ANNEAL-REQ-019](settled-requirements.md#anneal-req-019-coverage-adequacy-is-enforced)). + +How the guards and correspondence evidence are encoded, proved, and divided +among rustc, Charon, Aeneas, and Anneal remains open. The semantic requirements +do not choose between Lean proof arguments, sidecar theorems, or another +enforcement mechanism. + +Specification adequacy differs for a property whose meaning is supplied by the +user. Anneal can check that the declared definition is propagated and +enforced, but cannot infer whether it expresses the user's intended business, +cryptographic, or protocol requirement. If a specification claims +correspondence with Rust, an FFI implementation, an ISA, or another external +semantics, its adequacy remains an explicit trust dependency. + +## Contextual refinement + +Whole-artifact composition and reusable abstraction verification make +different claims. + +A whole-artifact result may cover only the concrete call sites, generic +instances, and reachable behaviors in one compilation subject. This is useful, +but it does not by itself prove a library safe for every future downstream +client. + +A reusable safe-API soundness claim requires robust safety: the implementation +must remain sound under every type-correct safe use admitted by the API within +a stated semantic and compilation envelope. More generally, contextual +refinement requires every implementation behavior visible to a context in the +quantified envelope to be permitted by the declared interface. Clients in that +envelope may then rely on the interface without reopening the private +implementation. Rust's underlying requirement is broad—an API presented as +safe must be sound for every type-correct safe use—even when Anneal can +initially report only a narrower artifact result. + +Every interaction relevant to the claim must be mediated by the interface and +by the capabilities or resources transferred across it. The implementation may +not silently invalidate context-owned resources or impose caller obligations +which the interface does not declare. This is not literal absence of +interaction, and the relevant boundary need not be a lexical scope. Allocators, +I/O, atomics, locks, nondeterminism, and other domains may expose deliberate +effects through effectful or resource-aware interfaces. + +The abstraction boundary may still be a pure value-level contract when that is +faithful. Contextual refinement requires it to preserve every observation and +discipline relevant to the claim; it does not require all unsafe +implementations to masquerade as pure functions. + +How Anneal exports and checks quantified contracts across separate compilation +remains open. Until it can establish that stronger claim, it must report the +narrower client envelope rather than silently generalize one artifact's +evidence. + +## Behavior remains part of the claim + +Anneal must support programs that return, panic safely, unwind through +soundness-relevant cleanup, catch a panic and continue, or execute indefinitely +while preserving invariants on every finite prefix. Verification therefore +cannot always mean normal termination. + +The proof model must distinguish enough source behavior to justify the +selected claim. It does not yet decide whether soundness, panic freedom, +termination, and other distinctions are built-in property kinds, standard +policies, effects in a weakest-precondition model, or user-defined predicates. +See [property kinds and outcomes](open-questions/property-kinds-and-outcomes.md). + +A model or tool failure is not a source-program behavior. It may create an +unsupported or incomplete result, but may never be interpreted as evidence +that the source satisfies a property. diff --git a/anneal/agent_docs/design/worked-example.md b/anneal/agent_docs/design/worked-example.md new file mode 100644 index 0000000000..0be3657f36 --- /dev/null +++ b/anneal/agent_docs/design/worked-example.md @@ -0,0 +1,226 @@ + + +# Worked example: an unsafe-backed byte buffer + +This schematic example connects the concepts in the +[verification model](verification-model.md) and +[result and trust model](result-and-trust.md). It is a teaching example, not a +normative design: `ByteBuffer`, the primitive leaves, predicates, proof +decomposition, outcome names, and result presentation below are all +illustrative. Names such as `BufferInvariant`, `owns`, and +`AbstractSequence` are explanatory notation rather than proposed Anneal or Lean +syntax. Open choices remain governed by the +[open-question ledger](open-questions/README.md). + +## The example abstraction + +Imagine a crate with this safe interface: + +```rust +pub struct ByteBuffer { /* private raw-pointer representation */ } + +impl ByteBuffer { + pub fn replace(&mut self, index: usize, value: u8) -> u8; +} +``` + +Internally, `ByteBuffer` owns a heap allocation and records a raw pointer, +length, and capacity. A schematic implementation of `replace` is: + +1. if `index >= len`, panic before touching the raw allocation; +2. otherwise call an unsafe primitive that replaces the byte at + `ptr + index` and returns the previous byte; and +3. return the previous byte. + +This resembles an implementation using `ptr::replace`, but the example does +not assert that `ptr::replace` should be Anneal's actual semantic leaf. + +## The trusted primitive leaf + +Suppose the Anneal standard library currently treats a primitive operation +called `replace_byte` as a trusted leaf. Its safety guard requires that: + +- the pointer identifies a live allocation with suitable provenance; +- the selected address is in bounds and properly aligned; +- the selected byte is initialized; and +- the caller holds exclusive authority to write that byte. + +The leaf's illustrative resource transition is: + +```text +owns(allocation, bytes) * index < length(bytes) + -- replace_byte(index, value) --> +owns(allocation, bytes[index := value]) * old = bytes[index] +``` + +Here `*` is only mnemonic notation for resource composition. Crucially, +`owns(allocation, bytes)` is consumed and replaced by the operation. It is not +an ordinary hypothesis that a proof may duplicate and use for two writes. The +exact resource logic or monadic machinery needed to enforce this discipline is +an [open design question](open-questions/memory-resources-and-effects.md). + +The primitive specification is trusted only at this boundary. Anneal must +still generate and check the guard at each call, and the ledger must identify +the specification as trusted. A future lower-level memory model could prove +the same leaf contract and remove that trust without changing `ByteBuffer`'s +public contract. + +## The type invariant + +For an abstract byte sequence `xs`, imagine an internal invariant with two +components: + +```text +BufferInvariant(buffer, xs) := + there is one live allocation described by buffer.ptr/len/capacity + * buffer has the exclusive owns(allocation, bytes) capability + * buffer.len = length(xs) + * the initialized prefix of bytes equals xs +``` + +The ownership component is soundness-relevant and resource-bearing. The +sequence relation supports an illustrative user-defined property, +`AbstractSequence`. A final design might represent those components together +or separately; this example does not decide that question. + +Holding a mutable reference to a valid `ByteBuffer` allows its implementation +to open the invariant according to controlled rules. It does not give arbitrary +proof code two copies of `owns`. Before control leaves the method normally or +by unwinding through relevant cleanup, the invariant must be available in the +state required at that boundary. + +Constructors must establish the invariant. Mutating methods must transform and +restore it. Destruction must consume the allocation capability exactly once. +Checking only `replace` while leaving construction, other field mutation, or +destruction unguarded would not establish the abstraction's soundness. + +## Contracts at the safe boundary + +The safe method has **no caller obligation whose violation permits undefined +behavior**. Every type-correct safe caller may pass any `usize`. In particular, +`index < len` is not a Rust safety precondition of `replace`. + +The API can nevertheless have ordinary outcome and functional contracts. One +illustrative contract says: + +- if `index` is out of bounds, the method panics without changing the abstract + sequence; +- if the method returns normally, the return value is the old byte at + `index`, and the new abstract sequence differs only by storing `value` at + that index; and +- throughout either behavior, the method remains sound. + +A caller seeking a no-panic result could prove the ordinary condition +`index < len`. Failure to prove that condition means the no-panic claim is +unavailable; it must not turn the safe call into undefined behavior. Whether +Anneal presents no-panic as a built-in policy, a property kind, or some other +construct remains open. + +## Local proof obligations + +For this example, a single symbolic execution could produce the following +obligations. That shared execution is illustrative rather than a commitment to +the final proof architecture. + +### Entry + +- Obtain `BufferInvariant(buffer, xs)` under the rules for a mutable borrow. +- Retain exactly one allocation capability while the invariant is open. + +### Out-of-bounds branch + +- Show that no raw-memory primitive is invoked. +- Show that the buffer state still represents `xs`. +- Under the artifact's unwind strategy, show that cleanup observes all + invariants and capabilities needed for soundness. +- Establish the contract's panic behavior. No normal-return postcondition is + claimed on this branch. + +### In-bounds branch + +- Derive every `replace_byte` guard from the branch condition and the opened + invariant; a user-written postcondition cannot substitute for a missing + provenance, initialization, or ownership fact. +- Apply the leaf's resource transition once. +- Re-establish `BufferInvariant(buffer, xs[index := value])` with the returned + allocation capability. +- Establish that the returned byte equals `xs[index]`. + +### Exit + +- Restore the invariant before returning control to safe code. +- Record dependencies between the user-defined `AbstractSequence` result and + the foundational soundness proof. + +Whether these facts are enforced through propositional arguments in translated +Lean definitions, sidecar WP theorems, or another complete mechanism remains +[unresolved](open-questions/source-model-adequacy.md). The requirement is that +Anneal cannot omit the primitive guard or a relevant control-flow branch. + +## Panic and unwind + +Because the bounds check occurs before the invariant is opened for mutation, +the panic branch has an unchanged buffer. With an unwind panic strategy, the +model must nevertheless follow cleanup and destruction far enough to prove +that resources remain valid and are consumed correctly. A panic is a source +behavior, not a verifier failure. + +Thus this method may satisfy soundness for every index while failing a blanket +no-panic claim. If a particular artifact uses `panic=abort`, the artifact and +claim differ; a proof for the unwind build is not automatically a proof for the +abort build. The example says nothing about whether outcome distinctions +become first-class axes in the final interface. + +Long-running behavior does not arise in this method. A server loop would use +the same general compositional idea but prove invariant preservation over each +finite execution prefix rather than require normal termination. + +## Global composition + +Assume that the artifact also proves: + +- every constructor establishes `BufferInvariant`; +- every other safe operation preserves it for all type-correct uses; +- destruction consumes its allocation exactly once; +- every call to a trusted memory or allocation leaf establishes that leaf's + guard; and +- no relevant item or control-flow edge is skipped. + +The local results then compose. Safe clients can use `ByteBuffer` without +examining its raw-pointer implementation or proving `index < len` for +soundness. The artifact is sound relative to the recorded primitive +specifications, translation adequacy, toolchain, and environmental assumptions. +If `AbstractSequence` is selected, clients may also use the proved sequence +contract without reopening the representation. + +This composition does not prove that a trusted leaf specification matches +Rust, that a user chose a useful abstract sequence contract, or that an +unchecked artifact variant has the same behavior. Those are different trust, +specification-adequacy, and artifact-identity questions. + +## An illustrative result record + +One fictional result for this example might be summarized as follows. The +record is intentionally compact; it demonstrates how the subject, claim, +evidence, and residual dependencies fit together rather than proposing a +schema. + +| Part | Illustrative contents | +| --- | --- | +| Compilation subject | `byte-buffer 0.1.0` at revision `abc123`; target `x86_64-unknown-linux-gnu`; feature `checked-replace`; compiler-resolved `cfg`; locked dependencies; `panic=unwind`; expanded generated Rust; relevant environment inputs | +| Claim | Soundness for the covered artifact, plus `AbstractSequence` for normal returns from `replace`; no claim over other targets, features, panic strategies, dependency resolutions, or downstream clients | +| Checked evidence | Constructors establish `BufferInvariant`; relevant methods preserve it; destruction consumes the allocation once; every covered memory-leaf call establishes its guard; `replace` proves its sequence contract | +| Residual dependencies | Trusted allocation, deallocation, and `replace_byte` specifications; no user axioms, incomplete proofs, prose justifications, or unsupported coverage in this fictional run | +| Provenance | Exact Anneal, Charon, Aeneas, rustc, LLVM, Lean, and proof-library identities and options, plus relevant host and target platform assumptions | + +If an incremental run relied only on prose for the `replace_byte` call, that +fact would move into the residual dependencies rather than checked evidence. +The eventual command-status policy remains open, but the conditional +dependency could not disappear from the reported result. See the canonical +[result and trust model](result-and-trust.md). diff --git a/anneal/agent_docs/glossary.md b/anneal/agent_docs/glossary.md new file mode 100644 index 0000000000..612b85cfec --- /dev/null +++ b/anneal/agent_docs/glossary.md @@ -0,0 +1,247 @@ + + +# Glossary + +This glossary gives short definitions for vocabulary stable enough to use +throughout the Anneal design. Proposed taxonomies remain in +[open design questions](design/open-questions/README.md) until accepted. + +## Assurance and properties + +**Soundness** + +: A guarantee that the covered Rust behavior has no undefined behavior. A safe + abstraction is sound only when every type-correct safe use admitted by its API + within the stated semantic and compilation envelope preserves that guarantee; + checking selected clients supports a narrower artifact claim. Soundness is + also a prerequisite for Anneal's promised source-to-model correspondence. + +**Unsafe (Rust)** + +: Rust syntax which marks an operation as carrying obligations the compiler + does not check, or marks a region in which the programmer accepts + responsibility for such obligations. The presence of `unsafe` code does not + by itself mean that the program is unsound. + +**Unsound** + +: Capable of causing Rust undefined behavior in a use which the relevant API + presents as permitted. An implementation may use `unsafe` operations and + still be sound when it establishes every required condition. + +**Property** + +: A proposition Anneal is asked to establish about a program or its behavior. + Examples include soundness, panic freedom, functional correctness, protocol + conformance, and resource bounds. + +**Property kind** + +: A class of obligations which may have its own contracts, invariants, + dependencies, and selection policy. Soundness is necessarily special; which + other classes receive first-class treatment remains open. + +**User-defined correctness property** + +: A property's intended meaning as supplied by the user rather than fixed by + Rust. Anneal can check a precise specification, but cannot decide whether it + expresses what the user actually wanted. + +**Specification adequacy** + +: Whether a specification is strong and faithful enough to justify the claim + made from it. In particular, a weak user contract must not erase a Rust + soundness requirement which Anneal is responsible for generating. + +## Claims, contracts, and composition + +**Claim** + +: The precise statement a verification result supports. It identifies the + Rust subject, properties, relevant behavior, coverage, and assumptions; “this + program is verified” without those qualifications is not a complete claim. + +**Contract** + +: The requirements under which an item may be used and the guarantees it + provides. A contract may mention multiple properties or execution outcomes; + its final source syntax remains open. + +**Precondition / caller obligation** + +: A requirement which must hold before an operation. At a call site, the caller + must establish each selected precondition—for example, that a pointer refers + to live memory. Rust safety requirements and ordinary functional assumptions + may require different source-language treatment even when Lean represents + both as propositions. + +**Postcondition** + +: A guarantee established after an operation for a relevant outcome. Which + outcomes carry which guarantees is part of the open property/outcome design. + +**Local guarantee** + +: What is proved about one item: under its preconditions, it establishes its + postconditions and meets the preconditions of the operations it invokes. + +**Global guarantee** + +: A claim obtained by composing local guarantees across the covered program, + relative to its explicitly reported trusted leaves and environmental + assumptions. + +**Robust safety** + +: The implementation remains sound under every type-correct safe use admitted + by its API within an explicitly stated semantic and compilation envelope. + This is the soundness-specific instance of the broader + contextual-refinement requirement. A result covering only selected clients + or calls is an artifact-level claim, not robust safety. + +**Contextual refinement** + +: Every implementation behavior visible to a context in the claim's quantified + envelope is permitted by the declared interface, including its stated effects + and transferred resources. Clients can therefore use the interface without + inspecting the private body. Checking the calls present in one compiled + program is narrower than proving this property for every client in such an + envelope; a result must say which claim it establishes. + +## Invariants and resources + +**Invariant** + +: A condition attached to a program abstraction which its rules require at + specified boundaries. Those rules determine when the condition may be + assumed, opened, consumed, and re-established. + +**Type invariant** + +: An invariant associated with values or storage of a type. Type invariants may + express arbitrary property kinds, and their enforcement must cover every + operation which can make the invariant relevant. + +**Trait invariant** + +: An invariant, of any property kind, which each relevant implementation of a + trait must establish and code with the corresponding trait bound may use. + +**Resource proposition** + +: A proposition whose proof carries ownership, permission, or another usage + discipline, so it cannot necessarily be copied or discarded like an + ordinary fact. Exclusive ownership and protocol state are common examples. + +**Capability** + +: Locally held authority or evidence which permits an operation, potentially + packaging facts about a heap, allocator, concurrency protocol, or external + environment. + +## Models, subjects, and evidence + +**Compilation subject (compilation artifact)** + +: One compiler-resolved Rust program with fixed target, features, `cfg` values, + dependencies, panic strategy, generated Rust, and relevant environment. It is + not a matrix of builds or merely Cargo's emitted native binary. + +**Verification result** + +: A reported claim about one compilation subject together with the checked + evidence and classified dependencies which support it. Proof-tool versions, + proofs, or assumptions can change the result without changing the Rust + subject. + +**Evidence graph** + +: The connected local contracts, proofs, call obligations, translation + evidence, and coverage evidence from which a result is composed. This is a + conceptual dependency graph; its concrete serialization remains open. + +**Residual dependency** + +: A dependency, gap, or failure which remains after Anneal evaluates the + evidence graph. It may condition or narrow a claim, or prevent Anneal from + establishing one. Examples include a trusted semantic leaf, an incomplete + proof, a prose justification, unsupported coverage, a toolchain dependency, + or an environmental assumption. Its status, role, and effect on the claim + must be explicit. + +**Source model** + +: The Lean-level semantics used to reason about the compiled Rust program. + Anneal must justify that this model is faithful for the claim it reports. + +**LLBC** + +: Charon's compiler-resolved, structured Rust intermediate representation. + Aeneas consumes LLBC, and current Anneal design work also trends toward + consuming it directly; the long-term integration boundary remains open. + +**Weakest-precondition specification (WP specification)** + +: A specification of what must hold before an operation so that a desired + continuation property holds afterward. Aeneas provides WP machinery and + tactics such as `step` and `step*` which Anneal should reuse when appropriate. + +## Trust and incompleteness + +**Trust** + +: A claim-relative reliance on a dependency whose correctness is not + established by checked evidence included in the result at the claimed + semantic endpoint. Trust can concern program semantics, correspondence and + integration, tool implementations, or the execution substrate. Not every + residual dependency is accepted as trust; some gaps and failures block a + claim instead. + +**Trusted computing base (TCB)** + +: Everything whose correctness must be assumed for a result to imply its + claim. This can include semantic leaves, translators, proof checking, + compilers, semantic assumptions, and relevant host and target hardware. + +**Trusted leaf** + +: An operation or external component whose specification is assumed rather + than proved from a body visible to the current verification. A deeper model + may replace that assumption later. + +**Axiom** + +: A proposition intentionally admitted without proof in the current model, + such as a specification of genuine external semantics or an Anneal-provided + primitive leaf. It must remain distinguishable in the result from an + unfinished proof or prose justification. Whether those categories share an + underlying Lean mechanism does not change their different meanings. + +**Incomplete proof** + +: A declared obligation whose proof has not yet been completed. It is different + from a claim that a proposition is inherently axiomatic. + +**Prose safety justification** + +: A human explanation, commonly a Rust `// SAFETY:` comment, accepted + temporarily in place of a selected formal proof during incremental adoption. + It is not a machine-checked theorem and must remain visible in the result. + +**Audit ledger** + +: The human- and machine-readable projection of the identities, residual + dependencies, coverage gaps, and trust assumptions which qualify a result. + Its exact schema remains open; its existence is required. + +**Fail closed** + +: Refuse to report a claim stronger than the available evidence supports. A + separately identified conditional or incremental result may still be useful + when every assumption and incomplete obligation is explicit. diff --git a/anneal/agent_docs/history/research-index.md b/anneal/agent_docs/history/research-index.md new file mode 100644 index 0000000000..1d213e1a5c --- /dev/null +++ b/anneal/agent_docs/history/research-index.md @@ -0,0 +1,184 @@ + + +# Anneal Research Index + +**Snapshot date: 2026-07-17.** + +Issues and pull requests record experiments, incomplete arguments, and views +which may already have changed. They are evidence and prompts for further +thinking, never normative design. Before relying on one, check its current +status, stack position, discussion, and diff. Normative constraints live in +[`agent_docs/design/`](../design/). + +## Coordinating issue + +[Tracking issue #3016](https://github.com/google/zerocopy/issues/3016) is the +best entry point into the work. At this snapshot it organizes work around: + +- making the implementation and infrastructure suitable for external + contribution; +- manually formalizing Rust from generated Lean in order to discover the + abstractions automation should eventually produce; +- separation-logic support in Aeneas; +- user-facing annotation and proof syntax; and +- internal code generation and organization. + +Its milestone and workstream wording is a planning snapshot, not a contract. +Use [principles](../design/principles.md), +[settled requirements](../design/settled-requirements.md), and the +[open-question index](../design/open-questions/README.md) to interpret it. + +## Open V2 and cross-cutting pull requests + +The following PRs were returned as open by a repository query on the snapshot +date. Many are GHerrit-managed stacked changes, so adjacent PRs can overlap or +be rebased together. Open status is not evidence that a change is absent from +this checkout: an open PR may be a stack ancestor or the current branch. +Inspect the tree and history to determine what is present, and use +[the current implementation state](../reference/current-state.md) for the +checked-in behavior rather than treating PR descriptions as authoritative. + +### Current orchestration and toolchain stack + +- [#3474: Compile merged util module at stack base](https://github.com/google/zerocopy/pull/3474) +- [#3463: Include Cargo in the exocrate Rust toolchain](https://github.com/google/zerocopy/pull/3463) +- [#3400: Add exocrate toolchain setup and `Toolchain` resolver](https://github.com/google/zerocopy/pull/3400) +- [#3401: Add Cargo workspace and target resolution](https://github.com/google/zerocopy/pull/3401) +- [#3402: Map workspace packages to `AnnealArtifact`s](https://github.com/google/zerocopy/pull/3402) +- [#3418: Add a pinned `charon_lib` dependency](https://github.com/google/zerocopy/pull/3418) +- [#3404: Add the Charon execution engine, `generate` CLI, and integration tests](https://github.com/google/zerocopy/pull/3404) +- [#3405: Chase out-of-tree dependencies for generation](https://github.com/google/zerocopy/pull/3405) +- [#3485: Prime Lake traces in one server traversal](https://github.com/google/zerocopy/pull/3485) +- [#3486: Audit cached Lean artifacts against clean builds](https://github.com/google/zerocopy/pull/3486) +- [#3403: Map compiler diagnostics back to Rust source](https://github.com/google/zerocopy/pull/3403) +- [#3436: Add an exocrate install-fixup hook](https://github.com/google/zerocopy/pull/3436) + +These changes are useful evidence about Cargo artifact identity, Charon +integration, diagnostics, cache portability, and the cost of dependency +chasing. They do not settle the long-term Anneal/Aeneas/Charon boundary. + +### Earlier or parallel V2 infrastructure + +- [#3361: Introduce Nix-based toolchain management](https://github.com/google/zerocopy/pull/3361) +- [#3362: Initial `setup` implementation](https://github.com/google/zerocopy/pull/3362) +- [#3378: Pass manifest and lockfile paths explicitly through exocrate](https://github.com/google/zerocopy/pull/3378) +- [#3487: Reorganize Anneal V1 and V2](https://github.com/google/zerocopy/pull/3487) + +Some effects of these proposals may already exist through different merged +commits. Read the current tree before assuming an open PR remains the intended +route. + +## Other open Anneal PRs: primarily V1 evidence + +These PRs were also open at the snapshot date. Most target the prototype or +pre-date the clean V2 boundary. They belong in historical research, not in the +V2 implementation plan by default. + +### Annotation, naming, and verification experiments + +- [#3478: Preserve module paths in generated function names](https://github.com/google/zerocopy/pull/3478) +- [#3477: Validate `isSafe` trait invariants while parsing](https://github.com/google/zerocopy/pull/3477) +- [#3321: Replace annotation syntax with verbatim Lean](https://github.com/google/zerocopy/pull/3321) +- [#3320: Translate and verify integration tests for the new syntax](https://github.com/google/zerocopy/pull/3320) +- [#3261: Add Lake package-management files](https://github.com/google/zerocopy/pull/3261) + +### Build, cache, and release experiments + +- [#3339: Remove redundant integration-test harness code](https://github.com/google/zerocopy/pull/3339) +- [#3338: Avoid copying Lean dependencies into the build directory](https://github.com/google/zerocopy/pull/3338) +- [#3337: Update integration tests for Nix](https://github.com/google/zerocopy/pull/3337) +- [#3336: Replace Docker with Nix](https://github.com/google/zerocopy/pull/3336) +- [#3335: WIP experimental changes](https://github.com/google/zerocopy/pull/3335) +- [#3334: WIP Docker-to-Nix conversion](https://github.com/google/zerocopy/pull/3334) +- [#3327: Download and install artifacts in parallel](https://github.com/google/zerocopy/pull/3327) +- [#3298: Adopt the Lake artifact cache and share workspace packages](https://github.com/google/zerocopy/pull/3298) +- [#3285: Overhaul release artifact and PR generation](https://github.com/google/zerocopy/pull/3285) +- [#3258: Roll prebuilts](https://github.com/google/zerocopy/pull/3258) +- [#3255: Reuse prebuilt Lean artifacts in generated workspaces](https://github.com/google/zerocopy/pull/3255) + +The repeated approaches are themselves evidence: setup latency, hermeticity, +Lake cache relocation, release provenance, and clean-build equivalence are +important engineering problems. No abandoned mechanism should be revived +solely because several old PRs explored it. + +## Issue map by research question + +The tracking discussion and repository issue search surfaced the following +threads. Open or closed status does not determine whether the underlying +question is settled. + +### Semantic coverage and artifact identity + +- [#3041: What about unreachable code?](https://github.com/google/zerocopy/issues/3041) + asks whether MIR elimination before Charon can hide code or produce a + misleading coverage claim. This is the concrete form of the question about + extraction before optimizations which assume or erase behavior. +- [#3017: Support `#[cfg]` in verification targets](https://github.com/google/zerocopy/issues/3017) + motivates making one resolved compilation artifact the source of truth. +- [#3350: Imported Rust types get unqualified names in generated specs](https://github.com/google/zerocopy/issues/3350) + illustrates the danger of a source-derived shadow naming system. + +### Trust, axioms, and proof completeness + +- [#3206: Ban axioms in non-axiom annotations](https://github.com/google/zerocopy/issues/3206) + is evidence for syntactic and semantic auditing of the Lean environment. +- [#3110: Visit all annotations and reject invalid locations](https://github.com/google/zerocopy/issues/3110) + concerns fail-closed coverage rather than only parsing supported locations. + +### Proof authoring and syntax + +- [#3201: Interactive proofs tracking](https://github.com/google/zerocopy/issues/3201) +- [#3062: Write Anneal specifications in Rust](https://github.com/google/zerocopy/issues/3062) +- [#3218: Make an entire annotation one Lean AST](https://github.com/google/zerocopy/issues/3218) +- [#3090: Pretty-print generated Lean](https://github.com/google/zerocopy/issues/3090) +- [#3086: Parse attributes with `chumsky`](https://github.com/google/zerocopy/issues/3086) +- [#3057: Support non-indented comments](https://github.com/google/zerocopy/issues/3057) + +These record syntax and tooling experiments. V2 has not selected a surface +language or proof location. + +### Hermeticity, packaging, and contributor workflow + +- [#3331: Manage all toolchain dependencies hermetically](https://github.com/google/zerocopy/issues/3331) +- [#3259: Build `Anneal.lean` independently in CI and locally](https://github.com/google/zerocopy/issues/3259) +- [#3256: Minimize dependencies of `Anneal.lean` and generated Lean](https://github.com/google/zerocopy/issues/3256) +- [#3266: Sanitize Cargo values used in Docker image creation](https://github.com/google/zerocopy/issues/3266) +- [#3420: Use standard base directories instead of polluting home directories](https://github.com/google/zerocopy/issues/3420) +- [#3060: Embed assets in the Anneal binary](https://github.com/google/zerocopy/issues/3060) + +Later Nix/exocrate work answers parts of these issues through different +mechanisms. Re-evaluate the underlying requirement rather than assuming the +issue's proposed implementation is still current. + +## Upstream reading + +- [Charon repository and documentation](https://github.com/AeneasVerif/charon) +- [Aeneas repository and documentation](https://github.com/AeneasVerif/aeneas) +- [Lean reference manual](https://lean-lang.org/doc/reference/latest/) +- [Rust Reference: behavior considered undefined](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) +- [Rust Unsafe Code Guidelines reference](https://rust-lang.github.io/unsafe-code-guidelines/) +- [RustBelt project and papers](https://plv.mpi-sws.org/rustbelt/) + +Read the pinned Aeneas and Charon revisions used by `flake.nix`, not only their +latest default branches. Anneal collaborates with both projects, so upstream +changes are possible; current upstream behavior remains distinct from a +proposed extension. The concise Anneal-specific division of responsibility is +in [Aeneas and Charon](../reference/aeneas-and-charon.md). + +## Maintaining this index + +When refreshing the snapshot: + +1. record the new date; +2. query current issue and PR state rather than copying this list; +3. preserve historically useful links under an explicitly historical heading; +4. summarize what question a source informs, not what decision it allegedly + dictates; and +5. move a conclusion into normative documentation only after the project has + actually accepted it. diff --git a/anneal/agent_docs/history/v1-lessons.md b/anneal/agent_docs/history/v1-lessons.md new file mode 100644 index 0000000000..d5cddc906e --- /dev/null +++ b/anneal/agent_docs/history/v1-lessons.md @@ -0,0 +1,196 @@ + + +# Lessons from Anneal V1 + +Anneal V1 is the experimental prototype in `anneal/v1/`. V2 is a clean-room, +ground-up redesign. V1 supplies observations, examples, and failure modes; it +does not supply defaults. Copy V1 code or concepts only after showing that they +serve V2's principles and current requirements. + +This page deliberately distills lessons rather than preserving every +terminological clarification made while discussing V1. + +## What the prototype demonstrated + +### A useful end-to-end workflow is possible + +V1 connected Rust source, Charon, Aeneas, generated Lean, user-authored +contracts, and the Lean checker. It demonstrated that a Cargo-facing tool can +keep formal obligations close to Rust code, automate the toolchain, and map +many failures back into a workflow recognizable to Rust engineers. + +That validates the product direction, not V1's particular annotation grammar, +source scanner, generated theorem shapes, or directory layout. + +### Aeneas's functional model is a powerful default + +For supported Rust, Aeneas turns disciplined borrowing and mutation into +mathematical value transformations. V1 showed the ergonomic payoff of using +that model for ordinary control flow surrounding unsafe leaves. V2 should +build on maintained Aeneas and Lean abstractions where they remain faithful, +including weakest-precondition specifications and existing tactics. + +The lesson is not that every behavior must be forced into a pure transformer. +Resource and effect semantics must remain explicit whenever erasing them +could undermine soundness. + +### Local contracts can support global reasoning + +V1's precondition/postcondition structure exercised the intended composition: +a caller proves a callee's requirements, and a callee proves what it returns +or preserves. This remains the core local shape from which artifact-wide +soundness and user-defined properties should be assembled. + +V1 did not prove the complete adequacy theorem connecting arbitrary unsafe +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 + +### Orthogonal progress and correctness duplicated work + +V1 split proofs into progress and correctness branches. The correctness branch +was conditional on successful execution, while the progress branch established +that execution succeeded. In practice: + +- the two proofs often repeated the same symbolic execution; +- the split did not compose naturally with Aeneas's WP specifications or its + `step` and `step*` tactics; and +- conditional correctness could be vacuous when progress was absent. + +V2 is leaning toward a shared Aeneas-style symbolic execution with obligations +for the relevant outcomes. The exact outcome/property architecture is still +open; V1 is evidence against making the orthogonal split the default, not a +decision that every verified function must terminate normally. + +Sound infinite execution, sound panic and unwind, and recovery after panic are +required use cases. + +### `isValid` was not enforced at mutation boundaries + +V1 attached an `isValid` predicate to a type and injected it into function +contracts, but safe Rust code could access or mutate invariant-carrying fields +without re-establishing the predicate. The mechanism was therefore knowingly +unsound and eventually required an explicit opt-in flag. + +V2 still requires type invariants for arbitrary property kinds. It must also +enforce opening and re-establishing them at every operation which can violate +them. Rust's proposed unsafe-fields feature could provide the language-level +boundary; Anneal-specific field access and mutation analysis is also in scope. +Waiting for upstream stabilization is not the only option. + +### `isSafe` expressed an architecture V1 did not enforce + +The durable idea behind V1's `isSafe` was that an unsafe trait implementation +establishes an invariant and generic code with the trait bound can consume it. +V1 documentation and implementation did not consistently enforce both halves. + +V2 requires trait invariants, like type invariants, to support arbitrary +property kinds. It must verify the invariant at every applicable +implementation site and expose exactly the corresponding assumption wherever +the trait bound is known. The final name and syntax are open. + +### Generated-Lean coupling was brittle + +V1 generated theorem signatures and proof scaffolding by predicting details +of Aeneas output: item names, tuple shapes, mutable-borrow returns, and special +treatment of `Unit` and `Never`. Small changes in Aeneas could require matching +Anneal changes or produce opaque Lean type errors. + +V2 should prefer compiler-resolved identities and maintained Aeneas interfaces +over textual surgery and a parallel source-derived ABI. This does not mandate +one interface: LLBC fields, library APIs, CLI modes, Lean syntax extensions, +and robust downstream adapters remain case-by-case options. + +### The source scanner could disagree with the compiler + +Parsing doc comments independently of rustc made it easy to lose the effects +of macro expansion, `cfg`, name resolution, aliases, and Cargo target +selection. A scanner can remain useful for source presentation, but semantic +claims must reconcile exactly with the compiler-selected artifact. + +### V1 annotation syntax is an experiment + +Indentation-sensitive Lean blocks in Rust documentation comments proved that +literate verification can work. They also exposed parser complexity, +formatting constraints, and leakage of Aeneas-generated names and proof +machinery. V2 is not committed to doc comments, indentation sensitivity, raw +Lean, Rust-like specifications, proof placement, or any V1 keyword. + +The audience requirement survives: ordinary Rust teams, including relatively +new engineers and engineers assisted by agents, must eventually be able to use +Anneal. Syntax should be judged by semantic clarity, diagnostics, +evolvability, and workflow—not resemblance to the prototype. + +## Trust-boundary lessons + +### `unsafe(axiom)` verified callers relative to a leaf + +V1's `unsafe(axiom)` made a function body opaque and trusted the user's +behavioral specification. It did not verify that body. This was useful for +composition and incremental coverage, but it left both the opaque +implementation and the specification in the TCB. + +V2's production objective is a small, explicit, shrinkable collection of +trusted leaves. Near-term leaves are expected to include some standard-library +unsafe operations and intrinsics, FFI, assembly, and raw-pointer operations. +Future formal ISA, foreign-language, or operational models may remove +individual leaves from the TCB. + +The syntax used for axioms is likely also needed by an Anneal standard library. +User-authored axioms will likely remain necessary for FFI for the foreseeable +future. It is open whether a foreign library author or each Rust consumer +normally owns those specifications. + +### Incomplete adoption needs a first-class status + +V1 supported `sorry`-based development and axiomatic boundaries, but a +production result needs to distinguish trusted external semantics from work +which is merely unfinished. Incremental adoption must also permit some +existing prose `// SAFETY:` justifications in place of formal proofs. + +Every such boundary must appear in an audit ledger. Whether an incomplete run +uses a separate command, profile, exit status, or result label remains open. + +### Specification adequacy cannot be delegated away + +Lean will prove a weak or vacuous specification. For Rust soundness, Anneal +must know or generate the required primitive safety obligations and ensure +that non-axiomatic specifications are adequate for them. Human review alone +is not an acceptable substitute for this mechanical guarantee. + +User-defined correctness properties have a different ground truth. Anneal can +ensure that a declared axiom is used and upheld, but cannot decide whether the +user chose the intended cryptographic, protocol, quantitative, or functional +property. + +## Product and reporting lessons + +- Rust's single `unsafe` axis is too coarse to express all property kinds. + Anneal must support dependencies among soundness and arbitrary additional + properties, while the degree of integration with Rust's existing unsafe + machinery remains open. +- Soundness is special and non-negotiable. Panic freedom, termination, + deadlock freedom, cryptographic correctness, resource bounds, and other + properties must not be silently conflated with it. +- A verification result needs an audit ledger. V1's opacity, axioms, `sorry`, + unsupported code, and toolchain assumptions were too easy to understand + only by inspecting implementation details. +- Diagnostics are part of semantic usability. When generated names or tuple + encodings leak into errors, users cannot reliably repair or review proofs. +- Incremental adoption is a core use case, but a partially checked result must + never masquerade as an unconditional one. + +## How to use V1 now + +Use `anneal/v1/` to reproduce experiments, inspect examples, and understand +why a V2 question exists. When citing it in a V2 design discussion, state the +observation rather than treating the V1 mechanism as precedent. If evidence +from V1 conflicts with [V2 principles](../design/principles.md) or +[settled requirements](../design/settled-requirements.md), V2 wins. diff --git a/anneal/agent_docs/reference/aeneas-and-charon.md b/anneal/agent_docs/reference/aeneas-and-charon.md new file mode 100644 index 0000000000..d58363fb5b --- /dev/null +++ b/anneal/agent_docs/reference/aeneas-and-charon.md @@ -0,0 +1,83 @@ + + +# Aeneas and Charon + +Anneal is being developed in collaboration with the +[Charon](https://github.com/AeneasVerif/charon) and +[Aeneas](https://github.com/AeneasVerif/aeneas) projects. This page records the +revision-sensitive facts coding agents need when working on that integration; +it does not assign future responsibilities among the projects. + +Upstream documentation and source are authoritative for a pinned release. This +page was last reviewed on 2026-07-17, when `anneal/flake.nix` selected Aeneas +release `nightly-2026.06.03`. Recheck the current pin before relying on a +supported construct, result type, or API described here. + +## Charon: compiler-integrated extraction + +Charon runs with the Rust compiler and exports Rust programs into LLBC (Low +Level Borrow Calculus), an intermediate representation designed for formal +reasoning. In the reviewed toolchain it provides compiler-resolved program +information after macro expansion and conditional compilation, including +resolved types, control flow, and source spans. + +Charon is not a verifier. Successful extraction means that it produced LLBC +for the selected compilation; it does not prove that the source is sound or +that a later Lean model is adequate. + +LLBC currently serves as Aeneas's semantic input. It can also provide +compiler-authoritative facts against which Anneal may reconcile annotations, +contracts, operations, calls, and diagnostics. Whether ordinary LLBC is +sufficient or another compiler-resolved interface is needed remains open. + +## Aeneas: functional translation and proof support + +Aeneas consumes LLBC and translates supported Rust into definitions in proof +assistants, including Lean. For a useful subset of Rust whose mutation follows +ordinary borrowing, this produces pure functional transformations rather than +an explicit whole-program heap model. Mutable-borrow translations carry the +information needed to reconstruct the final borrowed value. + +In the revision reviewed for this page, the Aeneas Lean library includes +weakest-precondition specifications and tactics such as `step` and `step*`. +Their exact interfaces and supported semantic envelope are revision-sensitive +and must be checked against the current pin. + +Aeneas does not by itself establish adequacy for every Rust program. Anneal's +questions about unsupported operations, resource-sensitive semantics, +exceptional execution, and the source-to-model correspondence are tracked in +the design documents linked below. + +## Checked-in Anneal integration + +The checked-in Anneal executable does not yet translate applications or verify +contracts. It currently packages and installs the pinned Aeneas distribution, +including the Aeneas and Charon executables and the Aeneas Lean libraries, and +constructs a Lean workspace which imports those libraries. See the +[current state](current-state.md) for the authoritative implementation summary. + +Anneal obtains the distribution from Aeneas's published +`nightly-2026.06.03` archive through `anneal/flake.nix`. The archive contains +Charon as part of the bundled toolchain; the checked-in setup does not maintain +a separate Charon pin. + +## Design questions owned elsewhere + +This reference intentionally does not decide what Charon should expose, what +semantics Aeneas should own, whether Anneal should extend either project, or +which downstream adaptations are acceptable. Those choices are governed by +the [project principles](../design/principles.md) and tracked in: + +- [Aeneas and Charon integration](../design/open-questions/aeneas-charon-integration.md); +- [source/model adequacy](../design/open-questions/source-model-adequacy.md); +- [memory, resources, and effects](../design/open-questions/memory-resources-and-effects.md); and +- [proof authoring and user experience](../design/open-questions/proof-authoring-and-user-experience.md). + +Experience from Anneal's earlier Aeneas integration is recorded separately in +[V1 lessons](../history/v1-lessons.md). diff --git a/anneal/agent_docs/reference/current-priorities.md b/anneal/agent_docs/reference/current-priorities.md new file mode 100644 index 0000000000..e8131d263f --- /dev/null +++ b/anneal/agent_docs/reference/current-priorities.md @@ -0,0 +1,108 @@ + + +# Current priorities + +**Snapshot date: 2026-07-17. This page is volatile and non-normative.** + +This page helps an agent apply Anneal's long-term principles to the early +implementation. It describes a useful near-term optimization lens, not an +accepted roadmap or a new ordering among the project's values. An explicit +task from the project authors, the [normative design](../README.md#normative-design), +and accepted decisions take precedence. + +## Starting point + +Read the dated [current implementation state](current-state.md) before planning +from this page. Establish what exists from the checked-in code and tests rather +than repeating a capability inventory here. + +Open and stacked pull requests explore nearby pipeline stages. They are useful +evidence about active engineering and integration pressure, but neither their +existence nor their implementation choices make them authoritative. Check the +current tree, tests, and history before claiming a capability has landed. The +[research index](../history/research-index.md) is only a dated navigation aid. + +## Near-term optimization lens + +Absent more specific direction, prefer work that turns the setup-only +foundation into a dependable, inspectable pipeline one reviewable stage at a +time. In practice, high-leverage work tends to have several of these +properties: + +- It makes the pinned Rust, Charon, Aeneas, Lean, and supporting artifacts + reproducible, installable, testable, or diagnosable. +- It connects a concrete Cargo compilation artifact to the next pipeline stage + through an explicit, machine-readable interface. +- It preserves compilation-subject identity and verification provenance rather + than relying on ambient state or an unreported default. +- It has a focused test that demonstrates the capability on the checked-in + branch and fails clearly when a dependency or stage is unavailable. +- It improves failure reporting and makes unsupported coverage or trust visible + rather than treating absence as success. +- It uses maintained Charon, Aeneas, Lean, Cargo, or rustc interfaces where + they fit, while keeping an upstream change in scope when that is the cleaner + long-term boundary. +- It is narrow enough to land without prematurely fixing an open semantic, + annotation, proof-authoring, or command-policy design. + +This lens favors durable enabling infrastructure over speculative completion +of the entire verifier. It does not make infrastructure more important than +soundness: any stage that begins making semantic claims must satisfy the +[settled requirements](../design/settled-requirements.md) and preserve the +[verification-result and trust model](../design/result-and-trust.md). + +## Working near the pipeline frontier + +Nearby work may involve Cargo target and artifact resolution, Charon execution, +LLBC transport, Aeneas generation, dependency discovery, Lake workspaces, +diagnostic mapping, or toolchain fixups. Treat that list as a description of +the engineering neighborhood, not a prescribed sequence or component boundary. + +For each change: + +1. Establish what is already present in this checkout; do not plan against a + sibling worktree or an open PR by accident. +2. Name the concrete input, output, and failure modes of the stage being added. +3. Preserve enough identity and provenance to relate its output to the fixed + [compilation subject and verification result](../design/result-and-trust.md). +4. Test the stage independently where practical and test the newly connected + boundary end to end. +5. Update current-state references only after the capability is checked in. +6. If the implementation would choose an answer recorded as open, pause for + explicit agreement or frame the work as a reversible experiment. + +In particular, pipeline plumbing must not incidentally settle the source of +annotation metadata, the Anneal/Aeneas/Charon ownership boundary, the unsafe +memory model, proof arguments versus sidecar theorems, or the final property +and outcome taxonomy. Those questions and their settled constraints live in +the [open-question index](../design/open-questions/README.md). + +## What not to optimize for yet + +Do not infer that the project currently wants: + +- a broad but unaudited claim of Rust coverage; +- compatibility with V1 syntax or architecture for its own sake; +- a polished `verify` success mode before its claim and trust reporting are + defined; +- local textual patches when a robust programmatic boundary is available; or +- premature generalization across target, feature, or configuration matrices + when the settled initial unit is one fixed compilation artifact. + +These cautions do not forbid experiments. They require experiments to be +identified as such and prevent temporary scaffolding from silently becoming a +project-wide decision. + +## Refreshing this page + +Revalidate this snapshot whenever the checked-in executable gains a pipeline +stage or project authors state a new near-term priority. Keep volatile work +sequencing here, current facts in the other `reference/` pages, and lasting +constraints or decisions in `design/`. Remove priorities that no longer help +choose work; do not preserve them as historical authority. diff --git a/anneal/agent_docs/reference/current-state.md b/anneal/agent_docs/reference/current-state.md new file mode 100644 index 0000000000..221704335a --- /dev/null +++ b/anneal/agent_docs/reference/current-state.md @@ -0,0 +1,157 @@ + + +# Current implementation state + +**Snapshot date: 2026-07-17.** + +This page describes the code checked into `anneal/`. It is a factual snapshot, +not a promise about the final architecture. Inspect the current tree and tests +when a detail matters; update this page when implementation changes make it +stale. + +## Status in one sentence + +Anneal currently constructs and installs its pinned external toolchain, but it +does not yet discover a Rust compilation subject, generate or check application +proofs, or produce a verification result. + +No invocation of the checked-in executable currently proves that an application +is safe or correct. + +## Repository boundary + +- `anneal/` contains the current clean-room implementation. +- `anneal/v1/` contains the historical prototype and has separate instructions. +- `exocrate/` installs and locates the versioned external toolchain archive. +- `.github/workflows/anneal.yml` contains jobs for both generations; passing a + V1 job does not establish a V2 capability. + +V1 remains useful implementation and design evidence. Its interfaces and +behavior are not defaults for the current implementation. + +## Implemented command path + +The compiled command currently supports `cargo-anneal setup`, including the +Cargo-plugin spelling `cargo anneal setup`. It selects either a local archive +provided with `--local-archive` or platform metadata from `Cargo.toml`, asks +`exocrate` to install or locate the archive, and reports the installation +directory. + +The checked-in remote archive URLs and hashes are placeholders. Development +and CI therefore use a locally constructed archive. `__ANNEAL_LOCAL_DEV` +selects a repository-local development installation; it is not a stable user +interface. + +`src/util.rs` contains helpers intended for later orchestration, but it is not +currently part of the compiled production command path. The presence of a +helper or an implementation in an open or sibling branch is not evidence that +the checked-in command exposes that capability. + +## Toolchain infrastructure + +`flake.nix` pins and packages a coupled Rust, Charon, Aeneas, Lean, Mathlib, and +supporting-tool environment for Linux and macOS on x86-64 and AArch64. It builds +Aeneas's Lean library, vendors Lake dependencies, prunes unused cache material, +normalizes selected paths and timestamps, and produces the omnibus archive used +by setup and CI. + +Supporting scripts rewrite vendored Lake metadata, prune the Mathlib closure, +derive coupled upstream versions and hashes, and check that release-relevant +flake outputs evaluate for every declared host system. These are substantial +toolchain and reproducibility capabilities; they are not an application +verification pipeline. + +## CI coverage + +The V2 CI path builds and layout-checks the omnibus archive, passes that exact +archive to the Rust test job, runs archive-dependent installation and Lake +cache tests, runs support-script tests, and evaluates the flake. Persistent Nix +caches written by pull requests are isolated from the cache populated by +trusted `main` builds. + +See [Development and CI](development-and-ci.md) for current commands, fixtures, +and workflow details. That page, the affected manifests, and the workflow files +are the closest sources of truth for validation. + +## Verification stages not yet implemented + +The checked-in executable does not yet: + +- select and identify a Cargo compilation subject; +- invoke Charon or consume LLBC; +- invoke Aeneas or generate a Lean model; +- resolve Anneal specifications or invariants; +- generate and track proof obligations; +- invoke Lean to check an application proof; +- map proof failures back to Rust source; +- compute property dependencies or coverage; or +- emit a scoped result and trust ledger. + +The intended high-level flow remains: + +```text +Cargo/rustc compilation subject + | + v + Charon extraction --> LLBC + | | + | v + | Aeneas Lean model + | | + +--------> Anneal contracts and obligations + | + v + Lean verification + | + v + scoped result and trust ledger +``` + +This diagram describes responsibilities, not settled APIs. Annotation +transport, unsafe-memory semantics, the Anneal/Aeneas/Charon boundary, proof +encoding, property representation, and command policy remain open. See the +[open-question index](../design/open-questions/README.md). + +## Current reporting and trust gaps + +Anneal does not yet produce a compilation-subject manifest, canonical result +identity, proof-coverage report, or audit ledger. It therefore does not yet +report residual trust in Charon, Aeneas, Anneal, Lean, rustc, LLVM, external +semantics, or host and target hardware. + +The toolchain archive pins many proof inputs, but the Rust toolchain used to +compile Anneal itself is not yet derived from the archive's pinned Rust +toolchain in CI. Placeholder download metadata also leaves the published +installation path incomplete. + +These are implementation limitations, not permission for a future verifier to +omit trust or coverage. The required result semantics live in +[Verification result and trust](../design/result-and-trust.md). + +## Using other sources + +Open issues and pull requests provide evidence about active work and design +pressure, but they do not describe the capabilities of this checkout. Before +claiming that a stage exists, inspect the checked-in implementation and tests. +Before treating an implementation choice as intended architecture, consult the +normative design documents and accepted decisions. + +The dated [current priorities](current-priorities.md) page is non-normative and +may help select near-term work. The [research index](../history/research-index.md) +is a navigation aid for issues and pull requests, not a capability ledger. + +## Updating this page + +Update this page when behavior lands, not when a pull request opens. Keep: + +- implemented facts here; +- commands and CI details in [Development and CI](development-and-ci.md); +- intended guarantees in `agent_docs/design/`; +- unresolved alternatives in `agent_docs/design/open-questions/`; and +- volatile work sequencing in [current priorities](current-priorities.md). diff --git a/anneal/agent_docs/reference/development-and-ci.md b/anneal/agent_docs/reference/development-and-ci.md new file mode 100644 index 0000000000..4c9c914706 --- /dev/null +++ b/anneal/agent_docs/reference/development-and-ci.md @@ -0,0 +1,146 @@ + + +# Development and CI + +Run V2 commands from `anneal/` or pass `--manifest-path anneal/Cargo.toml` +from the repository root. Commands rooted at `anneal/v1/` operate on the V1 +prototype. + +This page records the current workflow. It is not a stable CLI specification. + +## Fast local checks + +From the repository root: + +```bash +cargo test --locked --manifest-path anneal/Cargo.toml +PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover \ + -s anneal/tests -p 'test_*.py' +cargo fmt --manifest-path anneal/Cargo.toml --all -- --check +``` + +The repository-wide formatting entry point is: + +```bash +./ci/check_fmt.sh +``` + +That script intentionally formats V2, V1, `exocrate`, the workspace tools, +and Zerocopy. Use the narrower Cargo command while iterating on a V2-only +change; use the repository entry point before handing off a broad change. + +## Running setup locally + +The checked-in remote archive metadata is placeholder data. Exercise setup +with an archive built locally: + +```bash +mkdir -p anneal/target +nix build ./anneal#omnibus-archive-ci \ + --out-link anneal/target/anneal-exocrate.tar.zst +cargo run --manifest-path anneal/Cargo.toml -- \ + setup --local-archive anneal/target/anneal-exocrate.tar.zst +``` + +The archive argument is interpreted from the command's current directory. +When developing inside `anneal/`, use +`target/anneal-exocrate.tar.zst` instead. + +`__ANNEAL_LOCAL_DEV=1` selects the local-development installation location. +It is an internal switch and may change. + +## Archive-dependent Rust tests + +Tests behind the `exocrate_tests` feature expect this exact path relative to +`anneal/`: + +```text +target/anneal-exocrate.tar.zst +``` + +After building the archive, run: + +```bash +cargo test --locked --manifest-path anneal/Cargo.toml --all-features +``` + +These tests install the archive and build a small generated Lean workspace to +ensure the read-only, precompiled Lake cache can be reused. A missing archive +is a test-fixture failure, not evidence about Anneal's proof design. + +## Nix checks + +Evaluate every release-relevant flake package for every supported system: + +```bash +bash anneal/check-flake-eval.sh +``` + +Build and validate the archive for the current system: + +```bash +nix build ./anneal#omnibus-archive-ci +nix build ./anneal#omnibus-archive-layout-check --no-link +``` + +Evaluation across four systems is not a cross-platform build. CI's archive +builder builds for its current runner and separately checks that the package +graph evaluates for all declared systems. + +When rolling Aeneas, Rust, or Lean inputs, use +`anneal/chase-aeneas-versions.sh` as an aid. It downloads upstream artifacts +and computes coupled hashes. Review every resulting version and hash; Mathlib +cache output may require a subsequent fixed-output hash refresh. + +## CI topology + +`.github/workflows/anneal.yml` contains both generations: + +- `static_checks` runs V1 and V2 support-script tests and the V2 flake + evaluation check. +- `anneal_tests` and `verify_examples` are V1 jobs rooted at `anneal/v1/`. +- `v2_nix_cache` builds the V2 omnibus archive, checks its layout, and uploads + it for this workflow run. +- `v2` downloads that exact archive and runs + `cargo test --workspace --all-features` in `anneal/`. + +The Nix caches have a trust boundary. A cache saved by a trusted `main` build +may be reused by pull requests; a pull request writes only its PR-scoped +cache. Preserve that separation when changing cache keys or Actions steps. +The workflow artifact, not the persistent cache, is the cross-job handoff for +the current run. + +The release workflow currently publishes the V1 crate from `anneal/v1/` while +using V2's Nix flake to build omnibus toolchain archives. This mixed state is +intentional during the transition. Do not "simplify" paths without first +understanding which generation owns the crate and which owns the archive. + +## Platform-specific concerns + +- The flake declares Linux and macOS on x86-64 and AArch64. +- Linux builds use an FHS environment for downloaded Lean tooling. +- Ubuntu 24.04 CI temporarily adjusts an AppArmor user-namespace setting for + the sandboxed Nix build and restores it in an `always()` step. Preserve the + cleanup path. +- Lake metadata and trace files can contain build-machine absolute paths. + Archive construction deliberately rewrites them and makes the installed + Aeneas tree read-only. +- Archive size is checked against GitHub's release-asset limit. + +## Scope discipline + +Open stacked PRs contain scanner, Cargo resolution, Charon, generation, and +diagnostic work. When developing on a branch below those changes, use the +files actually present in the checkout as the source of truth. Do not add +tests or documentation for an API which only exists in another stack unless +the change explicitly depends on that stack. + +When a V2 change touches shared CI or release machinery, also run the relevant +V1 support tests. Otherwise, V1's large integration suite is not the default +validation target for V2 implementation work. diff --git a/anneal/v1/AGENTS.md b/anneal/v1/AGENTS.md index a0142e7794..18854514c3 100644 --- a/anneal/v1/AGENTS.md +++ b/anneal/v1/AGENTS.md @@ -6,11 +6,17 @@ license , at your option. This file may not be copied, modified, or distributed except according to those terms. --> -# Anneal +# Anneal V1 agent guide -> **Note to AI Agents:** This document is intended for agents **developing** the -> Anneal toolchain itself. If you are an agent **using** Anneal, please refer to -> the `llms.txt` and `docs/agent/` directory instead. +> **Historical prototype:** This file applies only to `anneal/v1/`. Anneal V2 +> is the clean-room redesign in the parent directory. V1 code, syntax, and +> architecture are not V2 defaults. Read the [V2 agent guide](../AGENTS.md) and +> [distilled V1 lessons](../agent_docs/history/v1-lessons.md) before carrying an +> idea from this subtree into V2. + +> **Note to AI Agents:** This document is intended for agents **developing the +> V1 prototype** itself. If you are an agent **using V1**, please refer to the +> `llms.txt` and `docs/agent/` directory instead. ## Basic commands diff --git a/anneal/v1/README.md b/anneal/v1/README.md index 66b7fd2811..a6e6bd5554 100644 --- a/anneal/v1/README.md +++ b/anneal/v1/README.md @@ -1,5 +1,12 @@ # Anneal +> **Historical V1 prototype:** This directory preserves Anneal V1 for +> maintenance, reproducibility, and design evidence. The active clean-room V2 +> redesign lives at [`anneal/`](../README.md). V1's syntax, architecture, +> soundness claims, and proof methodology are not commitments for V2. Coding +> agents comparing V1 with the current redesign must begin with the +> [current agent guide](../AGENTS.md). +

logo by tinyneonspark