From 76b033373e2c7427ab9f0e5ae1e9cd99aaa1990f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 24 Sep 2026 17:36:19 -0400 Subject: [PATCH 1/5] [anneal] Refine design contract semantics --- anneal/DESIGN.md | 354 ++++++++++++++++++++++------------------------- 1 file changed, 163 insertions(+), 191 deletions(-) diff --git a/anneal/DESIGN.md b/anneal/DESIGN.md index 0e8170979f..66c4f42d6c 100644 --- a/anneal/DESIGN.md +++ b/anneal/DESIGN.md @@ -8,201 +8,173 @@ those terms. --> # Anneal design contract -This document derives durable design constraints from Anneal's +This document derives design constraints from Anneal's [`PRINCIPLES.md`](PRINCIPLES.md). The principles define Anneal's promises, -beliefs, and rules for making decisions. This document states properties that -any Anneal design must preserve in order to uphold those principles. - -The principles are authoritative over this document. If the two conflict, the -principles win and this document must be corrected. Lower-level architecture, -implementation, and user-interface decisions must in turn be consistent with -both. - -This document intentionally stops short of choosing mechanisms. It does not -specify an annotation language, proof encoding, result schema, command-line -interface, or division of responsibility among Rust, Charon, Aeneas, Lean, and -Anneal. - -## Verification success has a precise meaning - -Anneal's promise is conditional but precise: if the code in a result's TCB is -correct, its trusted assumptions are valid, and Anneal emits no errors, then the -covered program behaves as promised. - -A successful verification result therefore needs enough identity and scope to -make that implication meaningful. It must identify the program or behavior to -which the result applies, the promises Anneal established, and the trusted code -and assumptions on which those promises depend. - -Anneal must never silently report a stronger promise than its evidence supports. -Missing evidence, unsupported semantics, omitted coverage, or a failed tool -cannot acquire the meaning of verification success merely because the pipeline -continued running. Development and incremental-adoption modes may expose useful -partial information, but their meaning must remain distinguishable from an -ordinary successful verification result. - -This constraint does not decide the atomic unit of verification, the exact -result format, or how command exit statuses represent incomplete work. - -## Rust-level claims require justified Rust semantics - -A theorem about a mathematical model supports a claim about Rust only when the -model is connected soundly to the Rust behavior being claimed. - -This matters especially for undefined behavior. Anneal cannot simply assume the -whole program is UB-free in order to obtain a faithful model and then cite a -theorem about that model as proof that the program is UB-free. Whatever model -and translation pipeline Anneal uses must provide a justified route from the -Rust program to the proof obligations whose discharge rules out undefined -behavior. - -In particular, any sound design must ensure both that: - -- the obligations Anneal requires are strong enough to establish the relevant - Rust validity conditions; and -- every operation and behavior relevant to the reported promise is accounted - for rather than disappearing because a model, translator, or proof interface - did not represent it. - -User-defined specifications cannot weaken or erase the Rust conditions needed -for well-defined behavior. Conversely, Anneal cannot determine whether a -user-defined property captures what its author intended; it can establish the -property that was actually specified. - -This document does not choose the proof of correspondence, the extraction point, -the unit of coverage, or which parts of that connection are initially proved -rather than trusted. - -## Verification composes through abstraction boundaries - -Anneal should let an implementation establish a promise once at an abstraction -boundary and let clients rely on that promise without reopening the private -implementation. - -For a safe Rust API, this includes Rust's existing soundness contract: no -hidden, unchecked obligation of a type-correct safe caller may determine whether -the implementation exhibits undefined behavior. An unsafe interface may place -explicit soundness obligations on its caller, just as Rust does today. - -The same compositional idea applies to promises beyond soundness. A function, -type, trait, module, crate, or other abstraction may expose requirements and -guarantees that clients can use without depending on its private proof details. -The exact set of useful abstraction boundaries remains a design question. - -An abstraction may hide implementation details only when doing so preserves all -semantics relevant to the promise. A pure value-level contract is preferable -when it is faithful. If ownership, provenance, initialization, concurrency, -protocol state, I/O, nondeterminism, or another effect matters to the promise, -the proof boundary must preserve enough of that structure to remain sound. -Simplifying the proof interface must not change the claim being proved. - -## Anneal is general over promises and program behaviors - -UB-freedom is foundational and always on, but it is not the only property Anneal -exists to prove. The architecture must allow developers to state and prove -additional correctness properties without baking today's anticipated set of -properties into a closed core. - -Different promises may require different semantic or proof machinery. Anneal -should share general machinery when the underlying reasoning is genuinely the -same, without forcing unrelated property domains into one representation that -loses important distinctions. +beliefs, and rules for making decisions. This document describes semantic +constraints that any Anneal design must preserve in order to uphold them. + +The principles are authoritative over this document. If the two conflict, this +document must be corrected. This document constrains the meaning of Anneal's +results and interfaces, not the mechanisms used to implement them. + +## Anneal proves conditional guarantees + +At a high level, an Anneal claim has: + +- a **subject** whose behavior is being verified; +- **requirements** under which the claim applies; and +- **guarantees** that hold when those requirements are satisfied. + +Anneal checks that the requirements imply the guarantees. That checked reasoning +is itself conditional on Anneal's trusted computing base (TCB). + +Requirements and TCB assumptions play different roles. A requirement is a +condition on the program's inputs, callers, or environment. It must be satisfied +when the claim is used. A TCB assumption is an unchecked premise in Anneal's +reasoning about whether the claim is true. + +Every fact Anneal itself needs to justify a reported claim must therefore either +be established by checked evidence or be represented explicitly in the TCB. A +required fact may not disappear merely because an analysis was skipped, +incomplete, unsupported, or failed. + +Why a fact is trusted does not change this core semantics. Anneal may record that +provenance for diagnostics, auditing, or policy, but an unfinished proof, an +external semantic assumption, and another unchecked premise are all trusted +premises at this level. + +Checked evidence about an intermediate model supports a Rust-level guarantee only +if the connection from Rust to that model is itself checked or included in the +TCB. An unchecked assumption does not stop being trusted merely because it is +encapsulated in a translator, generated artifact, helper library, compiler, or +other component. + +## Anneal connects source-level guarantees to compiled behavior + +Anneal ultimately makes claims about code produced by `rustc`, not only about an +intermediate mathematical model. + +Every successful Anneal result includes two baseline guarantees: + +1. the Rust executions covered by the claim are well-defined; and +2. subject to the TCB, the compiled code corresponds to the Rust source semantics + strongly enough to preserve the guarantees reported by Anneal. + +The second guarantee need not mean that the source and compiled program have +literally identical sets of behaviors. The required relationship is whatever is +strong enough to justify carrying each reported source-level guarantee to the +compiled code. + +Developers may ask Anneal to prove additional guarantees beyond well-definedness. +Those guarantees may themselves have requirements. For example, a safe binary +search function may guarantee that its result correctly reports membership only +when its input is sorted. Calling it with an unsorted slice may make that +additional guarantee inapplicable; it must not invalidate Anneal's baseline +guarantee that the safe call is well-defined. + +Proving a user-defined guarantee establishes the property that was specified. It +does not establish that the specification captures what its author intended. + +## Closed-program guarantees cover complete executions + +For a closed program, Anneal's well-definedness guarantee applies to complete +executions covered by the claim. + +Anneal may establish this guarantee using local proofs, component contracts, +whole-program reasoning, or another sound method. Regardless of the proof +strategy, those intermediate judgments must ultimately justify the whole-program +claim. Showing that one function or thread is locally well-behaved is insufficient +if another part of the same execution can exhibit undefined behavior. + +Additional developer-defined guarantees apply at the scope stated by their +claims. Anneal must not infer a whole-program guarantee from local facts that do +not establish it. + +## Library guarantees are contextual + +A library cannot guarantee the behavior of an arbitrary surrounding program. +Instead, Anneal verifies an implementation relative to an API contract. + +An API contract has: + +- **requirements** that a caller must satisfy and that the implementation may + assume; and +- **guarantees** that the implementation must establish and that a caller + satisfying the requirements may rely upon. + +Anneal's library guarantee is contextual: replacing the abstract API contract +with the verified implementation in an admissible context must preserve +well-definedness and the guarantees of that contract. In particular, if a context +interacting with the abstract contract has well-defined Rust behavior, then +replacing that contract with the verified implementation must not make the +resulting Rust execution undefined, provided the context satisfies the contract's +requirements. + +The exact formal account of this contextual relationship is a lower-level design +question. The guarantee must nevertheless be precise enough that it does not rely +on an informal judgment about whether undefined behavior was "caused by" or +"attributable to" the library. + +### Admissible use follows Rust's API conventions + +The choice of which contexts Anneal considers admissible is a policy choice, not a +mathematical necessity. Anneal chooses this boundary to align its formal +guarantees with Rust's conventions about what callers must establish and what API +implementations may assume. + +For a safe API, Anneal's baseline guarantees must hold for every use that: + +- is permitted by the Rust type system; and +- supplies values satisfying the invariants associated with their Rust types that + Rust convention permits implementations to rely upon. + +The second condition may be stronger than requiring that constructing or passing +the value has not already caused undefined behavior. For example, an +implementation receiving a `&str` may rely on the invariant that the `str` +contains valid UTF-8. + +A safe API may not impose any additional unchecked caller requirement needed for +Anneal's baseline well-definedness guarantee. A type-correct safe caller supplying +values that satisfy the applicable type invariants must not be able to violate +that guarantee merely because it failed to satisfy some hidden condition. + +Additional developer-defined guarantees may have additional preconditions. Those +preconditions limit only the corresponding additional guarantees; violating them +must not invalidate the baseline guarantee of a safe API. + +For an unsafe API, admissible use additionally requires satisfying the API's +explicit safety requirements. Anneal's baseline guarantee is conditional on those +requirements. + +By default, values passed to an unsafe API are also assumed to satisfy their +ordinary type invariants. Some unsafe APIs may need to accept values that violate +invariants normally associated with their types. Whether Anneal permits an unsafe +API contract to relax such an invariant, and how that permission is expressed, +remains unresolved. + +## Anneal is general over guarantees and program behaviors + +Anneal must allow developers to state and prove correctness guarantees beyond +well-definedness without fixing today's anticipated set of guarantees as a closed +universe. Anneal also aims to support all program *behaviors*, not every Rust source -program. It is acceptable for Anneal to reject a dark corner of Rust syntax or a -particular combination of features when the same intended behavior can be -expressed through a supported form. When practical, Anneal should give the -programmer actionable guidance for reaching that supported form. +program. It may reject particular language features or combinations of features +when the same intended behavior can be expressed in a supported way. When +practical, Anneal should give programmers actionable guidance toward such a form. -Supporting new properties and behaviors must not weaken the meaning of existing -successful results. +Adding support for new guarantees or program behaviors must not weaken the meaning +of existing successful verification results. ## The ordinary interface is Rust-oriented -Ordinary Rust programmers must be able to use Anneal effectively without -learning Lean 4. - -Anneal should present unsatisfied obligations in terms that connect directly to -the Rust program: what operation or promise generated the obligation, what must -be true, and what Anneal could not establish. The normal workflow should feel -like an extension of Rust's compiler-enforced reasoning rather than a demand -that every Rust programmer become a formal-methods specialist. - -This does not require hiding Lean or other proof machinery. Specialists may need -full access to Lean, Aeneas, resource logics, generated models, or other -low-level interfaces in order to prove novel properties or extend Anneal. -Those interfaces can coexist with a Rust-oriented ordinary path. - -Humans, coding agents, and other tools may also differ in how they author or -repair proofs. They must nevertheless operate against the same program -contracts, promises, trust model, and success semantics. A human explanation or -an agent's confidence is not machine-checked evidence merely because it is -persuasive; formal claims come from the accepted checking boundary. - -## Trust is explicit and replaceable by evidence - -Anneal cannot initially prove every fact on which an end-to-end result depends. -Everything whose correctness the result relies on but Anneal has not established -must remain visible as part of the relevant trusted computing base. - -Different kinds of missing evidence may have different consequences. A trusted -external semantic assumption, an unfinished proof, unsupported source behavior, -and a verifier failure need not be treated alike. The detailed taxonomy belongs -in lower-level design documentation, but the distinctions required to interpret -a result must not be erased by an implementation shortcut. - -Trust should also be shrinkable. A component or semantic assumption that is -trusted today should be replaceable by stronger checked evidence tomorrow -without requiring unrelated user contracts to be redesigned. Moving an -assumption into another helper, generated artifact, or upstream component does -not reduce trust unless the result no longer depends on its unchecked -correctness. - -## Prefer general, minimally sufficient mechanisms - -Anneal should use the simplest model that faithfully supports the promises being -made. - -When ordinary functional reasoning is sufficient, richer machinery should not -be imposed merely because Anneal must support harder cases elsewhere. When a -promise depends on ownership, effects, traces, concurrency, or other structure, -that structure must not be discarded merely to preserve a simpler proof model. - -Likewise, a practical example should normally be treated as evidence about a -broader class of problems. A one-off mechanism can be a useful experiment, but -it should not become architecture merely because it solves the first known use -case. Designs should leave room to increase expressive power and should prefer -reusable abstractions once the underlying problem is understood. - -Existing Rust, Lean, Charon, Aeneas, and ecosystem mechanisms are useful when -they solve the general problem faithfully. No particular ownership boundary or -integration technique is itself a principle: downstream adapters, upstream -changes, new libraries, and temporary experiments remain available when they -better preserve Anneal's promises. - -## Deliberate non-decisions - -This document constrains later design work without deciding it. In particular, -it does not currently determine: - -- the atomic subject of a verification result or how build matrices are handled; -- how generated Rust and other generated artifacts participate in a result; -- the taxonomy or selection model for properties and execution outcomes; -- whether type invariants, trait invariants, or other contract forms are - first-class Anneal concepts; -- the source syntax, location, or language used for specifications and proofs; -- whether obligations are represented as arguments, sidecar theorems, weakest - preconditions, or another proof encoding; -- the exact mechanism for prose-based or otherwise incremental adoption; -- the detailed classification of axioms, incomplete proofs, unsupported - behavior, coverage gaps, and tool failures; -- the contents or serialization of the TCB audit log; -- the meaning of particular command names, profiles, warnings, or exit codes; -- the boundary among Anneal, Rust, Charon, Aeneas, Lean, and reusable proof - libraries; or -- the exact theorem or validation strategy used to justify source/model - correspondence and complete obligation coverage. - -Those questions should be settled by later design work using the principles and -this contract as constraints. An implementation experiment may explore an -answer without silently turning that answer into a project-wide commitment. +Ordinary Rust programmers must be able to use Anneal effectively without learning +Lean 4. + +When Anneal cannot establish an obligation, its ordinary interface should connect +that failure to the Rust program: what operation or guarantee generated the +obligation, what must be true, and what Anneal could not establish. + +The normal workflow should therefore feel like an extension of Rust's existing +compiler-enforced reasoning rather than requiring every Rust programmer to become +a formal-methods specialist. From a4c6dd16292741bc8a3de0c727f47b5a845f21fd Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 24 Sep 2026 18:11:17 -0400 Subject: [PATCH 2/5] [anneal] Address design contract review feedback --- anneal/DESIGN.md | 110 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 80 insertions(+), 30 deletions(-) diff --git a/anneal/DESIGN.md b/anneal/DESIGN.md index 66c4f42d6c..a6b0f528e1 100644 --- a/anneal/DESIGN.md +++ b/anneal/DESIGN.md @@ -21,27 +21,61 @@ results and interfaces, not the mechanisms used to implement them. At a high level, an Anneal claim has: -- a **subject** whose behavior is being verified; +- a **scope** identifying the program artifacts, configurations, and executions + to which the claim applies; - **requirements** under which the claim applies; and -- **guarantees** that hold when those requirements are satisfied. +- **guarantees** that hold within that scope when those requirements are + satisfied. -Anneal checks that the requirements imply the guarantees. That checked reasoning -is itself conditional on Anneal's trusted computing base (TCB). +The scope must bind the claim unambiguously to what was actually verified. A +result for one revision, generated input, dependency set, feature configuration, +target, profile, compiled artifact, or other relevant input must not silently +apply to materially different code or configuration. A claim may cover a +precisely defined family rather than a single concrete build, but the result must +make that domain precise enough to determine whether a particular artifact or +execution is covered. + +Anneal checks that the requirements imply the guarantees for that scope. That +reasoning is itself conditional on Anneal's trusted computing base (TCB). Requirements and TCB assumptions play different roles. A requirement is a condition on the program's inputs, callers, or environment. It must be satisfied when the claim is used. A TCB assumption is an unchecked premise in Anneal's reasoning about whether the claim is true. -Every fact Anneal itself needs to justify a reported claim must therefore either -be established by checked evidence or be represented explicitly in the TCB. A -required fact may not disappear merely because an analysis was skipped, -incomplete, unsupported, or failed. +## Successful verification also constrains trust + +Every fact Anneal itself needs to justify a reported claim must either be +established by checked evidence or represented explicitly in the TCB. + +That condition alone is not sufficient for verification success. Otherwise, +Anneal could turn an obligation it failed to prove into a new trusted assumption +and report success without having provided the assurance the user requested. + +A verification result therefore also has an **assurance policy**: a constraint on +which unchecked premises may appear in the TCB while the result still counts as +successful. Any premise that the policy requires Anneal to establish must remain +outside the TCB and be supported by checked evidence. + +The assurance policy need not enumerate every intermediate lemma individually. +It may instead identify trusted components, semantic boundaries, classes of +assumptions, guarantees that must be established end-to-end, or other principled +boundaries. The exact way users, projects, or Anneal itself specify this policy is +a lower-level design question. + +An unfinished proof, skipped analysis, unsupported operation, or failed tool does +not authorize new trust merely by occurring. If the missing fact is not permitted +by the applicable assurance policy, Anneal has not produced a successful result. -Why a fact is trusted does not change this core semantics. Anneal may record that -provenance for diagnostics, auditing, or policy, but an unfinished proof, an -external semantic assumption, and another unchecked premise are all trusted -premises at this level. +Development workflows may deliberately use weaker assurance policies. Such a +result must remain distinguishable from a result satisfying the intended +verification policy; in particular, bypassing required UB checks must not silently +acquire the meaning of ordinary verification success. + +At the logical level, trusted premises are simply premises: why a fact is trusted +does not change the conditional theorem Anneal has established. Its identity, +provenance, or origin may nevertheless matter to the assurance policy, diagnostics, +auditing, or other higher-level interpretation of the result. Checked evidence about an intermediate model supports a Rust-level guarantee only if the connection from Rust to that model is itself checked or included in the @@ -57,14 +91,20 @@ intermediate mathematical model. Every successful Anneal result includes two baseline guarantees: 1. the Rust executions covered by the claim are well-defined; and -2. subject to the TCB, the compiled code corresponds to the Rust source semantics - strongly enough to preserve the guarantees reported by Anneal. +2. subject to the TCB, the behavior of the compiled artifact corresponds to the + Rust source semantics strongly enough to preserve the guarantees reported by + Anneal. The second guarantee need not mean that the source and compiled program have literally identical sets of behaviors. The required relationship is whatever is strong enough to justify carrying each reported source-level guarantee to the compiled code. +The verification scope must bind this end-to-end claim to the source and compiled +artifacts, or precisely characterized families of artifacts, for which the +relationship was established. Verifying one source or build must not bless a +different binary merely because they occupy the same nominal project or package. + Developers may ask Anneal to prove additional guarantees beyond well-definedness. Those guarantees may themselves have requirements. For example, a safe binary search function may guarantee that its result correctly reports membership only @@ -122,34 +162,44 @@ mathematical necessity. Anneal chooses this boundary to align its formal guarantees with Rust's conventions about what callers must establish and what API implementations may assume. -For a safe API, Anneal's baseline guarantees must hold for every use that: +Two kinds of constraints on values must be distinguished: -- is permitted by the Rust type system; and -- supplies values satisfying the invariants associated with their Rust types that - Rust convention permits implementations to rely upon. +- **Rust language validity requirements** are conditions required by Rust's + abstract semantics for the value or execution itself to be well-defined. Anneal + cannot relax these requirements for either safe or unsafe APIs. +- **API or library invariants** may be stronger than Rust language validity. + Rust's conventions may permit an API implementation to rely on such an + invariant even though violating the invariant is not itself immediate undefined + behavior. Valid UTF-8 for `str` is an example. -The second condition may be stronger than requiring that constructing or passing -the value has not already caused undefined behavior. For example, an -implementation receiving a `&str` may rely on the invariant that the `str` -contains valid UTF-8. +For a safe API, Anneal's baseline guarantees must hold for every use that: + +- is permitted by the Rust type system; +- satisfies Rust's language validity requirements; and +- supplies values satisfying the API or library invariants that Rust convention + permits the implementation to rely upon. A safe API may not impose any additional unchecked caller requirement needed for -Anneal's baseline well-definedness guarantee. A type-correct safe caller supplying -values that satisfy the applicable type invariants must not be able to violate -that guarantee merely because it failed to satisfy some hidden condition. +Anneal's baseline well-definedness guarantee. A type-correct safe caller meeting +the applicable validity requirements and API invariants must not be able to +violate that guarantee merely because it failed to satisfy some hidden condition. Additional developer-defined guarantees may have additional preconditions. Those -preconditions limit only the corresponding additional guarantees; violating them +preconditions limit only the corresponding additional guarantees. Violating them must not invalidate the baseline guarantee of a safe API. For an unsafe API, admissible use additionally requires satisfying the API's explicit safety requirements. Anneal's baseline guarantee is conditional on those requirements. -By default, values passed to an unsafe API are also assumed to satisfy their -ordinary type invariants. Some unsafe APIs may need to accept values that violate -invariants normally associated with their types. Whether Anneal permits an unsafe -API contract to relax such an invariant, and how that permission is expressed, +Rust language validity requirements remain mandatory at an unsafe API boundary. +An `unsafe` contract cannot make a value or execution valid when Rust's language +semantics already makes it invalid. + +API or library invariants stronger than language validity are different. Some +unsafe APIs may legitimately need to accept values that violate invariants +normally associated with their types. Whether Anneal permits an unsafe API +contract to relax such an invariant, and how that permission is expressed, remains unresolved. ## Anneal is general over guarantees and program behaviors From c40555425d134d1099416ec593900a22dd5d4d0b Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 24 Sep 2026 18:30:52 -0400 Subject: [PATCH 3/5] [anneal] Refine claim and assurance model --- anneal/DESIGN.md | 219 ++++++++++++++++++++++++----------------------- 1 file changed, 113 insertions(+), 106 deletions(-) diff --git a/anneal/DESIGN.md b/anneal/DESIGN.md index a6b0f528e1..926aecf01b 100644 --- a/anneal/DESIGN.md +++ b/anneal/DESIGN.md @@ -19,101 +19,118 @@ results and interfaces, not the mechanisms used to implement them. ## Anneal proves conditional guarantees -At a high level, an Anneal claim has: +An Anneal claim has a **scope** and one or more **guarantee clauses**. -- a **scope** identifying the program artifacts, configurations, and executions - to which the claim applies; -- **requirements** under which the claim applies; and -- **guarantees** that hold within that scope when those requirements are +The scope identifies the program artifacts, configurations, and executions to +which the claim applies. + +Each guarantee clause has: + +- **requirements** under which the clause applies; and +- a **guarantee** that holds within the claim's scope when those requirements are satisfied. +Different guarantees may therefore have different requirements. A requirement +for an additional functional guarantee does not automatically become a +requirement for Anneal's baseline well-definedness guarantee. + The scope must bind the claim unambiguously to what was actually verified. A result for one revision, generated input, dependency set, feature configuration, target, profile, compiled artifact, or other relevant input must not silently -apply to materially different code or configuration. A claim may cover a -precisely defined family rather than a single concrete build, but the result must -make that domain precise enough to determine whether a particular artifact or -execution is covered. +apply to materially different code or configuration. -Anneal checks that the requirements imply the guarantees for that scope. That -reasoning is itself conditional on Anneal's trusted computing base (TCB). +A claim may cover a precisely defined family rather than a single concrete build. +In either case, its scope must be precise enough to determine whether a particular +artifact, configuration, and execution is covered. -Requirements and TCB assumptions play different roles. A requirement is a +Requirements and trusted assumptions play different roles. A requirement is a condition on the program's inputs, callers, or environment. It must be satisfied -when the claim is used. A TCB assumption is an unchecked premise in Anneal's -reasoning about whether the claim is true. +when the corresponding guarantee is used. A trusted assumption is an unchecked +premise in Anneal's reasoning that the guarantee follows from its requirements. + +## Successful verification has an auditable trust boundary -## Successful verification also constrains trust +Anneal establishes its claims using checked evidence and a trusted computing base +(TCB). Every fact Anneal itself needs to justify a reported claim must either be -established by checked evidence or represented explicitly in the TCB. +established by checked evidence or represented in the TCB. An unchecked +assumption does not stop being trusted merely because it is encapsulated in a +translator, generated artifact, helper library, compiler, or other component. -That condition alone is not sufficient for verification success. Otherwise, -Anneal could turn an obligation it failed to prove into a new trusted assumption -and report success without having provided the assurance the user requested. +Every successful result must expose, or immutably reference, the complete TCB on +which its guarantees depend. Trusted code and assumptions must be identified +precisely enough to determine what the result relies upon. A TCB may itself refer +to other immutable, auditable manifests rather than duplicating their contents, +but trust must not disappear behind an implementation boundary. -A verification result therefore also has an **assurance policy**: a constraint on -which unchecked premises may appear in the TCB while the result still counts as -successful. Any premise that the policy requires Anneal to establish must remain -outside the TCB and be supported by checked evidence. +Merely recording every unchecked premise is not sufficient for verification +success. Otherwise, Anneal could fail to prove an obligation, add that obligation +to the TCB, and report success without providing the assurance the user requested. -The assurance policy need not enumerate every intermediate lemma individually. -It may instead identify trusted components, semantic boundaries, classes of -assumptions, guarantees that must be established end-to-end, or other principled -boundaries. The exact way users, projects, or Anneal itself specify this policy is -a lower-level design question. +A successful result is therefore also evaluated against an **assurance policy**. +The assurance policy constrains which unchecked premises may appear in the TCB +while the result still counts as successful. It may identify trusted components, +semantic boundaries, classes of assumptions, guarantees that must be established +by checked evidence, or other principled trust boundaries. + +The result must identify the assurance policy under which it reports success, so +that its actual TCB can be interpreted against that policy. An unfinished proof, skipped analysis, unsupported operation, or failed tool does -not authorize new trust merely by occurring. If the missing fact is not permitted -by the applicable assurance policy, Anneal has not produced a successful result. +not by itself authorize new trust. If the resulting unchecked premise is not +permitted by the applicable assurance policy, Anneal has not produced a successful +result. -Development workflows may deliberately use weaker assurance policies. Such a -result must remain distinguishable from a result satisfying the intended -verification policy; in particular, bypassing required UB checks must not silently -acquire the meaning of ordinary verification success. +The project principles impose minimum assurance requirements independent of any +user-selected policy. In particular, bypassing a required UB obligation cannot +silently become ordinary verification success by moving that obligation into the +TCB. Development workflows may deliberately accept weaker assurance, but their +results must remain distinguishable from ordinary successful verification. At the logical level, trusted premises are simply premises: why a fact is trusted -does not change the conditional theorem Anneal has established. Its identity, -provenance, or origin may nevertheless matter to the assurance policy, diagnostics, -auditing, or other higher-level interpretation of the result. +does not change the conditional claim Anneal has established. Its identity or +provenance may nevertheless matter to the assurance policy, auditing, diagnostics, +or other interpretation of the result. Checked evidence about an intermediate model supports a Rust-level guarantee only -if the connection from Rust to that model is itself checked or included in the -TCB. An unchecked assumption does not stop being trusted merely because it is -encapsulated in a translator, generated artifact, helper library, compiler, or -other component. +if the connection from Rust to that model is itself checked or represented in the +TCB. ## Anneal connects source-level guarantees to compiled behavior Anneal ultimately makes claims about code produced by `rustc`, not only about an intermediate mathematical model. -Every successful Anneal result includes two baseline guarantees: +Every successful Anneal result includes baseline guarantee clauses establishing +that: 1. the Rust executions covered by the claim are well-defined; and 2. subject to the TCB, the behavior of the compiled artifact corresponds to the - Rust source semantics strongly enough to preserve the guarantees reported by - Anneal. + Rust source semantics strongly enough to preserve the guarantees Anneal + reports. The second guarantee need not mean that the source and compiled program have literally identical sets of behaviors. The required relationship is whatever is strong enough to justify carrying each reported source-level guarantee to the compiled code. -The verification scope must bind this end-to-end claim to the source and compiled -artifacts, or precisely characterized families of artifacts, for which the +The claim's scope must bind this end-to-end guarantee to the source and compiled +artifacts, or precisely characterized families of artifacts, for which that relationship was established. Verifying one source or build must not bless a -different binary merely because they occupy the same nominal project or package. +different binary merely because they belong to the same nominal project or +package. Developers may ask Anneal to prove additional guarantees beyond well-definedness. -Those guarantees may themselves have requirements. For example, a safe binary -search function may guarantee that its result correctly reports membership only -when its input is sorted. Calling it with an unsorted slice may make that -additional guarantee inapplicable; it must not invalidate Anneal's baseline -guarantee that the safe call is well-defined. +Those guarantees may have their own requirements. For example, a safe binary +search function may guarantee correct membership results only when its input is +sorted. Calling it with an unsorted slice makes that guarantee inapplicable; it +does not invalidate Anneal's baseline guarantee that the safe call is +well-defined. -Proving a user-defined guarantee establishes the property that was specified. It -does not establish that the specification captures what its author intended. +Proving a developer-defined guarantee establishes the property that was +specified. It does not establish that the specification captures what its author +intended. ## Closed-program guarantees cover complete executions @@ -124,83 +141,73 @@ Anneal may establish this guarantee using local proofs, component contracts, whole-program reasoning, or another sound method. Regardless of the proof strategy, those intermediate judgments must ultimately justify the whole-program claim. Showing that one function or thread is locally well-behaved is insufficient -if another part of the same execution can exhibit undefined behavior. +if another part of the same covered execution can exhibit undefined behavior. -Additional developer-defined guarantees apply at the scope stated by their -claims. Anneal must not infer a whole-program guarantee from local facts that do -not establish it. +Additional developer-defined guarantees apply at the scopes and under the +requirements stated by their guarantee clauses. Anneal must not infer a +whole-program guarantee from local facts that do not establish it. ## Library guarantees are contextual A library cannot guarantee the behavior of an arbitrary surrounding program. -Instead, Anneal verifies an implementation relative to an API contract. +Instead, Anneal verifies an implementation relative to an API contract and +quantifies its guarantees over **admissible contexts**. -An API contract has: +An API contract contains guarantee clauses just like any other Anneal claim. Its +requirements are conditions a caller must satisfy and that the implementation may +assume. Its guarantees are conditions the implementation must establish and that a +caller satisfying the corresponding requirements may rely upon. -- **requirements** that a caller must satisfy and that the implementation may - assume; and -- **guarantees** that the implementation must establish and that a caller - satisfying the requirements may rely upon. +An admissible context must itself have well-defined Rust behavior when interacting +with the abstract API contract. This already excludes contexts that violate Rust's +language-level requirements for well-defined execution; an API contract cannot +make behavior defined that Rust semantics already makes undefined. Anneal's library guarantee is contextual: replacing the abstract API contract -with the verified implementation in an admissible context must preserve -well-definedness and the guarantees of that contract. In particular, if a context -interacting with the abstract contract has well-defined Rust behavior, then -replacing that contract with the verified implementation must not make the -resulting Rust execution undefined, provided the context satisfies the contract's -requirements. +with the verified implementation in an admissible context must preserve the +baseline well-definedness guarantee and the other guarantees whose requirements +the context satisfies. The exact formal account of this contextual relationship is a lower-level design -question. The guarantee must nevertheless be precise enough that it does not rely -on an informal judgment about whether undefined behavior was "caused by" or +question. It must be precise enough that the guarantee does not depend on an +informal judgment about whether undefined behavior was "caused by" or "attributable to" the library. ### Admissible use follows Rust's API conventions -The choice of which contexts Anneal considers admissible is a policy choice, not a -mathematical necessity. Anneal chooses this boundary to align its formal -guarantees with Rust's conventions about what callers must establish and what API -implementations may assume. - -Two kinds of constraints on values must be distinguished: - -- **Rust language validity requirements** are conditions required by Rust's - abstract semantics for the value or execution itself to be well-defined. Anneal - cannot relax these requirements for either safe or unsafe APIs. -- **API or library invariants** may be stronger than Rust language validity. - Rust's conventions may permit an API implementation to rely on such an - invariant even though violating the invariant is not itself immediate undefined - behavior. Valid UTF-8 for `str` is an example. +Well-defined Rust behavior alone does not capture every assumption that Rust +convention permits an API implementation to make. -For a safe API, Anneal's baseline guarantees must hold for every use that: +Some Rust APIs rely on **API or library invariants** that are stronger than the +language requirements for well-defined execution. For example, Rust libraries may +assume that a `str` contains valid UTF-8 even though constructing a non-UTF-8 +`str` is not itself immediate undefined behavior. -- is permitted by the Rust type system; -- satisfies Rust's language validity requirements; and -- supplies values satisfying the API or library invariants that Rust convention - permits the implementation to rely upon. +For a safe API, Anneal's baseline guarantee must hold for every well-defined, +type-correct use that also satisfies the API or library invariants that Rust +convention permits the implementation to rely upon. -A safe API may not impose any additional unchecked caller requirement needed for -Anneal's baseline well-definedness guarantee. A type-correct safe caller meeting -the applicable validity requirements and API invariants must not be able to -violate that guarantee merely because it failed to satisfy some hidden condition. +A safe API may not impose an additional hidden caller requirement needed for its +baseline well-definedness guarantee. A caller meeting the conditions above must +not be able to trigger undefined behavior merely because it failed to satisfy some +other unstated condition. -Additional developer-defined guarantees may have additional preconditions. Those -preconditions limit only the corresponding additional guarantees. Violating them -must not invalidate the baseline guarantee of a safe API. +Additional developer-defined guarantees may have additional requirements. Those +requirements limit only their corresponding guarantees; violating them must not +invalidate the baseline guarantee of a safe API. For an unsafe API, admissible use additionally requires satisfying the API's explicit safety requirements. Anneal's baseline guarantee is conditional on those requirements. -Rust language validity requirements remain mandatory at an unsafe API boundary. -An `unsafe` contract cannot make a value or execution valid when Rust's language -semantics already makes it invalid. +Because an admissible context must already be well-defined under Rust semantics, +an unsafe API cannot relax a condition whose violation is itself already undefined +behavior. -API or library invariants stronger than language validity are different. Some -unsafe APIs may legitimately need to accept values that violate invariants -normally associated with their types. Whether Anneal permits an unsafe API -contract to relax such an invariant, and how that permission is expressed, -remains unresolved. +Stronger API or library invariants are different. Some unsafe APIs may legitimately +need to accept values that violate invariants normally associated with their +types. Whether Anneal permits an unsafe API contract to relax such an invariant, +and how that permission is expressed, remains unresolved. ## Anneal is general over guarantees and program behaviors From c64bcf8e1dda3694ed292be17950aea67e9d6bf0 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 24 Sep 2026 19:09:17 -0400 Subject: [PATCH 4/5] [anneal] Stabilize verification result semantics --- anneal/DESIGN.md | 49 ++++++++++++++++++++++++++++++++++++------------ 1 file changed, 37 insertions(+), 12 deletions(-) diff --git a/anneal/DESIGN.md b/anneal/DESIGN.md index 926aecf01b..434845d3c0 100644 --- a/anneal/DESIGN.md +++ b/anneal/DESIGN.md @@ -17,6 +17,27 @@ The principles are authoritative over this document. If the two conflict, this document must be corrected. This document constrains the meaning of Anneal's results and interfaces, not the mechanisms used to implement them. +## Verification results have stable meaning + +An ordinary successful Anneal result fixes three things: + +- the **claim** Anneal established; +- the complete **trusted computing base (TCB)** on which that claim depends; and +- the **assurance policy** under which that TCB was accepted. + +Everything whose identity can affect the meaning of the claim or whether the +result qualifies as successful must be fixed by the result, either directly or +through an immutable reference. + +A later change to source code, generated input, a specification, a dependency, a +TCB manifest, an assurance policy, or another referenced input must not +retroactively change what an existing result means or whether it qualified as +successful when produced. + +Mutable names and configuration such as branches, profiles, or named policies may +be convenient inputs to verification. A result that depends on them must bind the +specific identities or contents that were actually used. + ## Anneal proves conditional guarantees An Anneal claim has a **scope** and one or more **guarantee clauses**. @@ -50,8 +71,7 @@ premise in Anneal's reasoning that the guarantee follows from its requirements. ## Successful verification has an auditable trust boundary -Anneal establishes its claims using checked evidence and a trusted computing base -(TCB). +Anneal establishes its claims using checked evidence and a TCB. Every fact Anneal itself needs to justify a reported claim must either be established by checked evidence or represented in the TCB. An unchecked @@ -74,19 +94,25 @@ while the result still counts as successful. It may identify trusted components, semantic boundaries, classes of assumptions, guarantees that must be established by checked evidence, or other principled trust boundaries. -The result must identify the assurance policy under which it reports success, so -that its actual TCB can be interpreted against that policy. +The result must contain or immutably reference the exact assurance policy under +which it reports success. A mutable policy name may select a policy before +verification, but later changes to that name must not alter the interpretation of +an existing result. An unfinished proof, skipped analysis, unsupported operation, or failed tool does not by itself authorize new trust. If the resulting unchecked premise is not permitted by the applicable assurance policy, Anneal has not produced a successful result. -The project principles impose minimum assurance requirements independent of any -user-selected policy. In particular, bypassing a required UB obligation cannot -silently become ordinary verification success by moving that obligation into the -TCB. Development workflows may deliberately accept weaker assurance, but their -results must remain distinguishable from ordinary successful verification. +The project principles impose minimum assurance requirements that an assurance +policy cannot weaken. In particular, a required UB obligation cannot become an +ordinary successful verification result merely by moving that obligation into the +TCB. + +Anneal may provide development-only modes that bypass UB checks or turn them into +warnings. Such outputs do not have ordinary successful-verification semantics and +must clearly label both the result and its TCB audit log as tainted or irreparably +untrustworthy, as required by `PRINCIPLES.md`. At the logical level, trusted premises are simply premises: why a fact is trusted does not change the conditional claim Anneal has established. Its identity or @@ -106,9 +132,8 @@ Every successful Anneal result includes baseline guarantee clauses establishing that: 1. the Rust executions covered by the claim are well-defined; and -2. subject to the TCB, the behavior of the compiled artifact corresponds to the - Rust source semantics strongly enough to preserve the guarantees Anneal - reports. +2. the behavior of the compiled artifact corresponds to the Rust source semantics + strongly enough to preserve the guarantees Anneal reports. The second guarantee need not mean that the source and compiled program have literally identical sets of behaviors. The required relationship is whatever is From 11def47d4ea97077f097f90b11db73156372286e Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 24 Sep 2026 19:15:33 -0400 Subject: [PATCH 5/5] [anneal] Simplify design contract organization --- anneal/DESIGN.md | 309 ++++++++++++++++++++++------------------------- 1 file changed, 144 insertions(+), 165 deletions(-) diff --git a/anneal/DESIGN.md b/anneal/DESIGN.md index 434845d3c0..4d02b0aef9 100644 --- a/anneal/DESIGN.md +++ b/anneal/DESIGN.md @@ -8,245 +8,224 @@ those terms. --> # Anneal design contract -This document derives design constraints from Anneal's +This document derives semantic constraints from Anneal's [`PRINCIPLES.md`](PRINCIPLES.md). The principles define Anneal's promises, -beliefs, and rules for making decisions. This document describes semantic -constraints that any Anneal design must preserve in order to uphold them. +beliefs, and rules for making decisions. This document defines what Anneal's +results must mean in order to uphold them. -The principles are authoritative over this document. If the two conflict, this -document must be corrected. This document constrains the meaning of Anneal's -results and interfaces, not the mechanisms used to implement them. +The principles are authoritative. If this document conflicts with them, this +document must be corrected. It constrains semantics, not the mechanisms used to +implement them. -## Verification results have stable meaning +## What an Anneal claim means -An ordinary successful Anneal result fixes three things: +An Anneal claim identifies: -- the **claim** Anneal established; -- the complete **trusted computing base (TCB)** on which that claim depends; and -- the **assurance policy** under which that TCB was accepted. - -Everything whose identity can affect the meaning of the claim or whether the -result qualifies as successful must be fixed by the result, either directly or -through an immutable reference. +- a **scope**: the program artifacts, configurations, and executions to which the + claim applies; and +- one or more **guarantees**, each with any **requirements** under which that + guarantee applies. -A later change to source code, generated input, a specification, a dependency, a -TCB manifest, an assurance policy, or another referenced input must not -retroactively change what an existing result means or whether it qualified as -successful when produced. +A requirement is a condition on the program's inputs, callers, or environment. +Different guarantees may have different requirements. A requirement for an +additional functional guarantee therefore does not become a requirement for +Anneal's baseline well-definedness guarantee. -Mutable names and configuration such as branches, profiles, or named policies may -be convenient inputs to verification. A result that depends on them must bind the -specific identities or contents that were actually used. +For example, a safe binary-search function may guarantee correct membership +results only when its input is sorted. Calling it with an unsorted slice makes +that guarantee inapplicable; it does not invalidate Anneal's guarantee that the +safe call is well-defined. -## Anneal proves conditional guarantees +The scope may describe one concrete build or a precisely defined family of +artifacts and configurations. In either case, it must be precise enough to +determine whether a particular artifact, configuration, and execution is covered. -An Anneal claim has a **scope** and one or more **guarantee clauses**. +Proving a developer-defined guarantee establishes the property that was +specified. It does not establish that the specification captures what its author +intended. -The scope identifies the program artifacts, configurations, and executions to -which the claim applies. +## What a successful result establishes -Each guarantee clause has: +An ordinary successful Anneal result fixes: -- **requirements** under which the clause applies; and -- a **guarantee** that holds within the claim's scope when those requirements are - satisfied. +- the exact **claim** Anneal established; +- the complete **trusted computing base (TCB)** on which that claim depends; and +- the exact **assurance policy** under which that TCB was accepted. -Different guarantees may therefore have different requirements. A requirement -for an additional functional guarantee does not automatically become a -requirement for Anneal's baseline well-definedness guarantee. +These must have stable meaning. Everything whose identity can affect the claim or +whether the result qualifies as successful must be contained in the result or +immutably referenced by it. -The scope must bind the claim unambiguously to what was actually verified. A -result for one revision, generated input, dependency set, feature configuration, -target, profile, compiled artifact, or other relevant input must not silently -apply to materially different code or configuration. +Mutable names such as branches, profiles, or named policies may be convenient +inputs to verification. The result must bind the specific artifacts, +specifications, configurations, policies, and other relevant inputs that were +actually used. Later changes to those inputs must not change the meaning or +success status of an existing result. -A claim may cover a precisely defined family rather than a single concrete build. -In either case, its scope must be precise enough to determine whether a particular -artifact, configuration, and execution is covered. +### The TCB contains all unchecked trust -Requirements and trusted assumptions play different roles. A requirement is a -condition on the program's inputs, callers, or environment. It must be satisfied -when the corresponding guarantee is used. A trusted assumption is an unchecked -premise in Anneal's reasoning that the guarantee follows from its requirements. +Every fact Anneal needs in order to justify a claim must either be established by +checked evidence or represented in the TCB. -## Successful verification has an auditable trust boundary +An unchecked assumption does not stop being trusted because it is encapsulated +inside a translator, generated artifact, helper library, compiler, or another +component. -Anneal establishes its claims using checked evidence and a TCB. +Every successful result must expose, or immutably reference, its complete TCB. +Trusted code and assumptions must be identified precisely enough to determine +what the result relies upon. The TCB may refer to other immutable, auditable +manifests rather than duplicating their contents, but trust must not disappear +behind an implementation boundary. -Every fact Anneal itself needs to justify a reported claim must either be -established by checked evidence or represented in the TCB. An unchecked -assumption does not stop being trusted merely because it is encapsulated in a -translator, generated artifact, helper library, compiler, or other component. +At the logical level, trusted premises are simply premises. Why a premise is +trusted does not change the conditional claim Anneal establishes, although its +identity and provenance may matter when deciding whether that trust is acceptable. -Every successful result must expose, or immutably reference, the complete TCB on -which its guarantees depend. Trusted code and assumptions must be identified -precisely enough to determine what the result relies upon. A TCB may itself refer -to other immutable, auditable manifests rather than duplicating their contents, -but trust must not disappear behind an implementation boundary. +### The assurance policy constrains acceptable trust -Merely recording every unchecked premise is not sufficient for verification -success. Otherwise, Anneal could fail to prove an obligation, add that obligation -to the TCB, and report success without providing the assurance the user requested. +Recording every unchecked premise is not enough to make verification successful. +Otherwise Anneal could fail to prove an obligation, add that obligation to the +TCB, and report success. -A successful result is therefore also evaluated against an **assurance policy**. -The assurance policy constrains which unchecked premises may appear in the TCB -while the result still counts as successful. It may identify trusted components, +The assurance policy defines which unchecked premises may appear in the TCB while +the result still counts as successful. It may identify trusted components, semantic boundaries, classes of assumptions, guarantees that must be established by checked evidence, or other principled trust boundaries. -The result must contain or immutably reference the exact assurance policy under -which it reports success. A mutable policy name may select a policy before -verification, but later changes to that name must not alter the interpretation of -an existing result. +A successful result must contain or immutably reference the exact assurance +policy against which its TCB was evaluated. A mutable policy name may select that +policy before verification, but changing the name's definition later must not +change an existing result. An unfinished proof, skipped analysis, unsupported operation, or failed tool does -not by itself authorize new trust. If the resulting unchecked premise is not +not itself authorize new trust. If the resulting unchecked premise is not permitted by the applicable assurance policy, Anneal has not produced a successful result. -The project principles impose minimum assurance requirements that an assurance -policy cannot weaken. In particular, a required UB obligation cannot become an -ordinary successful verification result merely by moving that obligation into the -TCB. +Anneal's principles also impose minimum assurance requirements that a policy +cannot weaken. In particular, a required UB obligation cannot become ordinary +verification success merely by moving it into the TCB. Anneal may provide development-only modes that bypass UB checks or turn them into -warnings. Such outputs do not have ordinary successful-verification semantics and -must clearly label both the result and its TCB audit log as tainted or irreparably -untrustworthy, as required by `PRINCIPLES.md`. +warnings. Such outputs are not ordinary successful verification results and must +clearly label both the result and its TCB audit log as tainted or irreparably +untrustworthy, as required by [`PRINCIPLES.md`](PRINCIPLES.md). -At the logical level, trusted premises are simply premises: why a fact is trusted -does not change the conditional claim Anneal has established. Its identity or -provenance may nevertheless matter to the assurance policy, auditing, diagnostics, -or other interpretation of the result. +## Every successful result makes an end-to-end Rust claim -Checked evidence about an intermediate model supports a Rust-level guarantee only -if the connection from Rust to that model is itself checked or represented in the -TCB. +Every ordinary successful result establishes at least that: -## Anneal connects source-level guarantees to compiled behavior +1. the Rust executions within its scope are well-defined; and +2. the behavior of the compiled artifact corresponds to the Rust source semantics + strongly enough to preserve every guarantee Anneal reports. -Anneal ultimately makes claims about code produced by `rustc`, not only about an -intermediate mathematical model. +The second guarantee does not require the source and compiled program to have +literally identical sets of behaviors. Their relationship need only be strong +enough to justify transferring the reported guarantees from source semantics to +compiled behavior. -Every successful Anneal result includes baseline guarantee clauses establishing -that: +A theorem about an intermediate model supports a Rust-level guarantee only when +the connection between Rust and that model is itself checked or represented in +the TCB. -1. the Rust executions covered by the claim are well-defined; and -2. the behavior of the compiled artifact corresponds to the Rust source semantics - strongly enough to preserve the guarantees Anneal reports. - -The second guarantee need not mean that the source and compiled program have -literally identical sets of behaviors. The required relationship is whatever is -strong enough to justify carrying each reported source-level guarantee to the -compiled code. - -The claim's scope must bind this end-to-end guarantee to the source and compiled -artifacts, or precisely characterized families of artifacts, for which that -relationship was established. Verifying one source or build must not bless a -different binary merely because they belong to the same nominal project or -package. - -Developers may ask Anneal to prove additional guarantees beyond well-definedness. -Those guarantees may have their own requirements. For example, a safe binary -search function may guarantee correct membership results only when its input is -sorted. Calling it with an unsorted slice makes that guarantee inapplicable; it -does not invalidate Anneal's baseline guarantee that the safe call is -well-defined. +The claim's scope must cover the source and compiled artifacts, or precisely +characterized families of artifacts, for which this end-to-end relationship was +established. Verifying one source or build must not bless a different binary +merely because both belong to the same nominal project or package. -Proving a developer-defined guarantee establishes the property that was -specified. It does not establish that the specification captures what its author -intended. +## Well-definedness depends on what is being verified + +Anneal's baseline well-definedness guarantee has the same purpose for closed +programs and libraries, but their scopes differ. -## Closed-program guarantees cover complete executions +### Closed programs -For a closed program, Anneal's well-definedness guarantee applies to complete -executions covered by the claim. +For a closed program, the guarantee applies to complete executions within the +claim's scope. -Anneal may establish this guarantee using local proofs, component contracts, -whole-program reasoning, or another sound method. Regardless of the proof -strategy, those intermediate judgments must ultimately justify the whole-program -claim. Showing that one function or thread is locally well-behaved is insufficient -if another part of the same covered execution can exhibit undefined behavior. +Anneal may establish this using local proofs, component contracts, whole-program +reasoning, or another sound method. Regardless of proof strategy, those +intermediate judgments must justify the whole-program guarantee. Showing that one +function or thread is locally well-behaved is insufficient if another part of the +same covered execution can exhibit undefined behavior. -Additional developer-defined guarantees apply at the scopes and under the -requirements stated by their guarantee clauses. Anneal must not infer a -whole-program guarantee from local facts that do not establish it. +Developer-defined guarantees apply only at the scopes and under the requirements +stated by the claim. Local facts must not be presented as whole-program guarantees +unless they establish them. -## Library guarantees are contextual +### Libraries A library cannot guarantee the behavior of an arbitrary surrounding program. -Instead, Anneal verifies an implementation relative to an API contract and -quantifies its guarantees over **admissible contexts**. +Anneal therefore verifies a library relative to an API contract and quantifies +its guarantees over **admissible contexts**. -An API contract contains guarantee clauses just like any other Anneal claim. Its -requirements are conditions a caller must satisfy and that the implementation may -assume. Its guarantees are conditions the implementation must establish and that a -caller satisfying the corresponding requirements may rely upon. +The API contract uses the same model as any other Anneal claim: its requirements +are facts a caller must establish and the implementation may assume; its +guarantees are facts the implementation must establish and a caller satisfying +the corresponding requirements may rely upon. An admissible context must itself have well-defined Rust behavior when interacting -with the abstract API contract. This already excludes contexts that violate Rust's -language-level requirements for well-defined execution; an API contract cannot -make behavior defined that Rust semantics already makes undefined. +with the abstract API contract. An API contract cannot make behavior defined that +Rust semantics already makes undefined. Anneal's library guarantee is contextual: replacing the abstract API contract -with the verified implementation in an admissible context must preserve the -baseline well-definedness guarantee and the other guarantees whose requirements -the context satisfies. +with the verified implementation in an admissible context must preserve +well-definedness and every other guarantee whose requirements that context +satisfies. -The exact formal account of this contextual relationship is a lower-level design -question. It must be precise enough that the guarantee does not depend on an -informal judgment about whether undefined behavior was "caused by" or -"attributable to" the library. +The lower-level formal model may express this relationship in different ways, but +it must not depend on an informal judgment that undefined behavior was "caused +by" or "attributable to" the library. -### Admissible use follows Rust's API conventions +#### Safe and unsafe API conventions Well-defined Rust behavior alone does not capture every assumption that Rust convention permits an API implementation to make. -Some Rust APIs rely on **API or library invariants** that are stronger than the -language requirements for well-defined execution. For example, Rust libraries may -assume that a `str` contains valid UTF-8 even though constructing a non-UTF-8 -`str` is not itself immediate undefined behavior. +Some APIs rely on **API or library invariants** stronger than Rust's requirements +for well-defined execution. For example, Rust libraries may assume that a `str` +contains valid UTF-8 even though constructing a non-UTF-8 `str` is not itself +immediate undefined behavior. For a safe API, Anneal's baseline guarantee must hold for every well-defined, -type-correct use that also satisfies the API or library invariants that Rust -convention permits the implementation to rely upon. +type-correct use that also satisfies the API or library invariants Rust convention +permits the implementation to rely upon. -A safe API may not impose an additional hidden caller requirement needed for its -baseline well-definedness guarantee. A caller meeting the conditions above must -not be able to trigger undefined behavior merely because it failed to satisfy some -other unstated condition. +A safe API may not impose any other hidden caller requirement needed for its +baseline well-definedness guarantee. A caller satisfying the conditions above +must not be able to trigger undefined behavior merely because some additional +unstated condition was false. -Additional developer-defined guarantees may have additional requirements. Those -requirements limit only their corresponding guarantees; violating them must not -invalidate the baseline guarantee of a safe API. +Other developer-defined guarantees may have additional requirements. Those +requirements constrain only their corresponding guarantees; they cannot weaken +the baseline guarantee of a safe API. For an unsafe API, admissible use additionally requires satisfying the API's explicit safety requirements. Anneal's baseline guarantee is conditional on those requirements. Because an admissible context must already be well-defined under Rust semantics, -an unsafe API cannot relax a condition whose violation is itself already undefined +an unsafe API cannot relax a condition whose violation is itself undefined behavior. -Stronger API or library invariants are different. Some unsafe APIs may legitimately -need to accept values that violate invariants normally associated with their -types. Whether Anneal permits an unsafe API contract to relax such an invariant, -and how that permission is expressed, remains unresolved. +Stronger API or library invariants are different. Some unsafe APIs may need to +accept values that violate invariants normally associated with their types. +Whether Anneal permits an unsafe API contract to relax such an invariant, and how +that permission is expressed, remains unresolved. -## Anneal is general over guarantees and program behaviors +## Anneal remains open-ended -Anneal must allow developers to state and prove correctness guarantees beyond -well-definedness without fixing today's anticipated set of guarantees as a closed -universe. +Well-definedness is mandatory, but developers must also be able to state and prove +additional correctness guarantees. Anneal must not fix today's anticipated +guarantees as a closed universe. -Anneal also aims to support all program *behaviors*, not every Rust source +Anneal likewise aims to support all program *behaviors*, not every Rust source program. It may reject particular language features or combinations of features when the same intended behavior can be expressed in a supported way. When -practical, Anneal should give programmers actionable guidance toward such a form. +practical, it should give the programmer actionable guidance toward such a form. -Adding support for new guarantees or program behaviors must not weaken the meaning -of existing successful verification results. +Adding support for new guarantees or behaviors must preserve the meaning of +existing successful results. ## The ordinary interface is Rust-oriented @@ -254,7 +233,7 @@ Ordinary Rust programmers must be able to use Anneal effectively without learnin Lean 4. When Anneal cannot establish an obligation, its ordinary interface should connect -that failure to the Rust program: what operation or guarantee generated the +the failure to the Rust program: what operation or guarantee generated the obligation, what must be true, and what Anneal could not establish. The normal workflow should therefore feel like an extension of Rust's existing