diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md new file mode 100644 index 0000000000..0f9968be5d --- /dev/null +++ b/verification/aeneas/ADMISSION_DESIGN.md @@ -0,0 +1,654 @@ + + +# Admitting Rust executions before Aeneas lowering + +This document records the correspondence design and its implementation boundary. +The current checker implements the restricted value-and-borrow fragment below. +The broader storage and handler rules remain requirements for future extensions, +not a claim that today's CI certifies arbitrary unsafe Rust. The +[lowering audit](LOWERING_AUDIT.md) records the remaining translator premises. + +## Implemented fragment + +`run.sh` requests promoted MIR from the pinned compiler. A checked-in Charon +patch saves its imported unstructured AST *before any Charon transformations*. +`admission.py` inspects that snapshot and final LLBC. It follows every function +binding and executable dependency, including original unwind and dead blocks. +A stock driver cannot silently skip the check: the missing snapshot rejects the +run. Drop terminators are rejected before drop elaboration or cleanup can erase +them. During admission, the driver refuses to fall back to optimized MIR for +local bodies if their requested MIR was stolen. We deliberately use promoted MIR +rather than drop-elaborated MIR; no supported execution relies on a destructor's +effects. + +The allowed operations are logical integers, booleans, field records, ordinary +arrays/slices, supported borrows, checked indexing/arithmetic, branching, and +loops. Unknown AST constructors and extraction options reject the run. Escaping +borrows, callbacks, raw pointers, foreign ABIs, statics, assembly, drops, union +storage, and general memory observations remain unsupported. Valid incoming +references and Aeneas's reviewed borrow translation are explicit premises. + +`external.json` supplies exact reviewed leaves, including standard-library +builtins and two local unsafe helpers. Local opaque body hashes are checked +against Rust-parser body boundaries. The only admitted generic transmutation +instantiation is `u8 -> bool`; its interpretation rejects all other bytes and +instantiations. Byte copying has explicit input and updated-output slices and +rejects oversized sources. Complete-definition checks in `Check.lean` compare +these interpretations and unchecked arithmetic independently, including bad +inputs. Generated external templates must retain failure-capable signatures; +normalization must not lose a guarded call. Pinned builtin mapping and backend +semantics remain trusted correspondence premises, rather than a translation +certificate established by the report. + +The report lives in the existing `bindings.json`. It includes both AST digests, +root coverage, visited executions, call boundaries, registry digest, source +identity, Cargo configuration hashes, and patched-runtime provenance. Compiler +overrides are rejected before compilation. A pre-compilation identity must match +at binding time and again after proof checking. Golden and live definitions +remain independent and receive the same complete proof and dependency audits. + +Current specifications permit no failure. Source UB aborts may still lower to +panic, but neither outcome is admitted by total or partial contracts. Unwind +paths can contain only non-executing cleanup bookkeeping and terminal failure; +any effectful cleanup rejects admission. There are no supported failure +handlers, spawned threads, or callbacks. A future recovery model must preserve +UB separately; do not infer that every generated panic is catchable Rust panic. + +`SafetyTests.lean` proves that sequencing preserves `.undef` and both execution +judgments reject it for arbitrary postconditions. It also checks invalid Boolean +production before discarding or divergence, and every oversized byte copy. +`tests/test_admission.py` mutates a real original extraction to challenge missing +registration, unsupported instantiation, annotated callees, drops, raw storage, +unknown effects/attributes/options, and failure-erasing signatures. Shell +controls challenge well-formed semantic mutations in both proof projects. +These tests establish sensitivity of the checks, not exhaustive rustc semantics. + +## Correspondence requirements for the fragment and future extensions + +The goal is to accept an extraction only when every operation in the executions +it describes has an adequate interpretation. Finding every annotation, preserving +every explicit call, or rejecting unsupported syntax is individually +insufficient. An implicit destructor can have an effect; a builtin can replace +a call incorrectly; a compiler pass can remove an operation before we inspect it. + +The design retains one checking path for every discovered specification. It +does not introduce special root declarations, a second roster of functions, or +per-function options to skip the safety checks. Unsupported cases fail the run. +It also retains ordinary mathematical decoders: no encoder, injectivity law, +or separate representation theorem becomes mandatory for each annotated type. + +The core rule is small: follow every executable dependency, and require either +an analyzed body from the controlled compilation or an explicitly reviewed +interpretation of that exact operation. Both must preserve failures as well as +successful behavior. Unknown origins or unsupported effects reject the run. +The rules below explain how to apply this rule before information disappears; +they do not add another specification language or another result type. + +## What a successful run would establish + +For a discovered function, begin with concrete Rust arguments represented by +the extracted arguments. The mathematical decoders must accept the arguments, +and the written requirements must hold. The caller must also supply the +well-formed Rust state required at the function boundary: valid input values +and, where references are present, the necessary ownership, allocation, +alignment, and interference conditions. A logical referent value alone is not +evidence for those conditions. + +Those boundary premises must not assume that the function being proved avoids +UB. In particular, an unsafe operation's guard must appear in its interpretation +and be established by the caller's proof. A general premise saying that every +internal access is valid would merely assume the desired conclusion. When the +current model cannot express the needed guard or frame, exclude the operation. + +Subject to the execution correspondence described below, a proved contract +then establishes the following for that invocation: + +- A total contract permits only successful termination, with the specified + postconditions and accepted output decoding. +- A partial contract also permits divergence. Every finite execution prefix + must still be free of UB. Panic and forbidden execution remain unacceptable. +- Neither contract permits UB before a result is discarded, before divergence, + or while executing a callee or implicit operation within the invocation. + +This is conditional safety, not proof that all safe Rust callers establish the +requirements. It does not certify a whole program, its unrelated threads, or a +value's later destruction by its caller. Native-process termination also needs +the runtime/resource premises of the chosen Rust execution model; an abstract +termination proof does not establish sufficient stack space on every machine. + +Bit-validity checks concern producing Rust values, including intermediate +ones. Library-model admission concerns which already-valid values a contract +describes. Failing the former must be an execution failure. Failing the latter +can exclude an input from a conditional contract. These cannot share a rule +that silently treats an invalidly produced Rust value as an excluded input. + +## The correspondence rule + +Use one relation between concrete Rust execution states and abstract states. +It records the observations and safety conditions needed by the admitted +operations. It can forget details, such as padding contents, if no admitted +operation relies on them. + +The required correspondence has three parts: + +1. Every concrete execution is covered, not merely the executions that happen + to return a value. A concrete prefix reaching UB must be incompatible with + the abstract contract. It cannot disappear into abstract success or + divergence. Ordinary failure is also incompatible with today's contracts. +2. Every concrete successful result is related to a modeled successful result, + with the observations needed for the written postconditions. If several + concrete results share one abstract value, the postcondition must apply to + all of them. Choosing one convenient result is not an abstraction argument. +3. For total contracts, concrete divergence cannot become abstract success. + Erased steps must not hide an infinite computation. A proof of progress, or + an explicitly trusted progress correspondence, is necessary as well as + preservation of successful values. + +To justify these properties compositionally, start from related entry states +without assuming the function's own safety. For each admitted operation, +establish that a permitted concrete step preserves the relation, or that its +bad case produces a failure before execution continues. Compose these local +rules through calls and control flow, including the progress rule for erased +steps. Together with the Lean contract's rejection of failure, they exclude +the first bad concrete step. Do not begin a simulation by assuming that the +entire concrete execution is already UB-free. + +This is a stronger requirement than an ordinary compiler correctness theorem +about preserving executions that were already defined. Rust optimizers may +assume UB never occurs and remove branches leading to it; the +[documentation for `unreachable_unchecked`](https://doc.rust-lang.org/std/hint/fn.unreachable_unchecked.html) +gives an explicit example. A correct optimizer is therefore not automatically +a suitable front end for proving absence of source-level UB. + +For example, consider this design witness: + +```rust +unsafe fn require_nonzero(x: usize) -> usize { + if x == 0 { + core::hint::unreachable_unchecked(); + } + 1 +} +``` + +Inspecting an optimized body that only returns `1` cannot justify a source +contract with no requirement on `x`. The admission mechanism must reject that +input body or rely on a separate interpretation of the original operation that +retains its requirement. A sound implementation must not assume the missing +requirement as part of its correspondence premise. + +The practical implementation will still trust pinned compiler/importer passes, +Aeneas's supported value-and-borrow semantics, selected backend definitions, +and reviewed external interpretations. These are named correspondence premises, +not Lean theorems supplied by the admission report. The checker is itself part +of the trusted infrastructure until its acceptance rule is formally verified. +No successful test suite makes those premises unconditional. + +## The pipeline and its single source of identity + +The existing annotation scan supplies the roots and Rust owners. Charon supplies +the final LLBC. A mandatory check runs on that LLBC before Aeneas can consume it. +The existing source-binding checks, conservative golden comparison, two proof +builds, required-contract checks, and compiled dependency audits then run. + +Extend the existing binding manifest with the admission result and the inputs +it actually checked: + +- Source/configuration identity and discovered Rust owners, including dependency + sources, the lockfile, target, Cargo features, effective `cfg` values, panic + strategy, overflow settings, and enabled target features. +- Toolchain pins, applied patches, extraction options, backend identity, and + the support-policy version. Anneal remains the source of truth for pins. +- The exact LLBC digest, extraction provenance, visited declarations and calls, + admitted external interpretations, and rejection reasons with source locations. + +The claim applies to that exact Rust configuration. A verification-only `cfg` +that substitutes a simpler function body cannot certify the production body. +Additional harnesses may be enabled for extraction, but any change to the +implementation or its dependencies is a different subject. Do not summarize +one verified target/feature selection as coverage of every build configuration. + +The manifest remains the one record connecting Rust owners, admission, and +generated declarations. Do not construct another root map or a separately +maintained roster of approved functions. The driver must check and lower the +same immutable LLBC snapshot. The proof builds must use the corresponding +generated modules and source bindings. The final completion record is written +only after all checks finish, and identifies both proof builds and their inputs. + +A report is evidence of running a trusted checker, not a translation certificate +checked by Lean. A cached report is reusable only for the same complete input +identity. Missing reports, changed inputs, stale compiled modules, skipped +audits, and development-only extraction are not successful CI verification. +The CI aggregate must require the completed run, rather than interpreting a +skipped job or `--extract-only` exit status as a proof result. + +Goldens retain their own definitions throughout checking. Admission of the fresh +LLBC concerns the live extraction; it does not establish a separate Rust +correspondence for an old golden. Both model builds independently pass proofs +and dependency checks. The application of those proofs to current Rust relies +on the live extraction's correspondence, not fuzzy text comparison. + +## Admit bodies by their origin + +There are two ways to justify an executable dependency: + +- Analyze its body, produced by the controlled compiler/importer pipeline, and + inspect its dependencies using the same rule. +- Select an exact external interpretation, with the guards, behavior, and + correspondence premises described below. A compiler builtin is such an + interpretation too; its familiar name does not exempt it from review. + +This is an evidence distinction, not a user choice between stronger and weaker +contracts. A body being present in LLBC does not establish its origin. A body +being absent does not establish that the function is harmless. Stop traversal +at a reviewed interpretation because that interpretation covers the operation, +not simply because the declaration is opaque or comes from the standard library. + +Choose evidence for the interpretation Aeneas actually uses. If a builtin +replaces a function whose body is present in LLBC, inspecting that Rust body +does not justify the replacement. The builtin needs the external-interpretation +case, with its replacement mapping and failure classification checked. An +analyzed body is admitted only when the reviewed translation uses that body. + +Start with freshly compiled local bodies and explicitly modeled external leaves. +An imported dependency body needs evidence that its MIR was produced by the +controlled pipeline. Otherwise give it an external interpretation or reject it. +Keep the existing default sysroot: rebuilding the entire standard library is +unnecessary when its admitted operations have reviewed external interpretations. +If a future proof needs a standard-library body, establish its build origin then. + +## Reuse Charon's MIR preservation configuration + +Most operation checks use information already present in final LLBC: calls, +operands, projections, residual drops, abort kinds, unwind blocks, function +attributes, types, constants, and trait evidence. Do not add a general earlier +AST export merely because Aeneas later erases some of that information. + +The pinned +[Charon MIR selector](https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/bin/charon-driver/translate/get_mir.rs#L60) +can silently fall back to optimized MIR when a requested local body has been +consumed. Non-local functions may also arrive as optimized MIR. The inspected +LLBC schema does not attest to the actual stage selected for each body. However, +the query name alone does not tell us which optional optimizations ran. + +The pinned [Charon driver already sets](https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/bin/charon-driver/driver.rs#L33) +`always_encode_mir = true`, `mir_opt_level = Some(0)`, and +`mir_preserve_ub = true`. Both selected-crate and normal dependency compilation +use this setup. Charon's Cargo command installs the driver as `RUSTC_WRAPPER` +for every crate it compiles. Reuse and validate that implementation rather than +adding duplicate command-line flags or an independently maintained compiler +preset. The existing toolchain provenance record already hashes the driver +and compiler binaries; Anneal remains the source of their pins. + +`-Copt-level=0` alone is insufficient: the compiler separately controls MIR +optimization, whose documented default in unoptimized builds is level 1. +The equivalent command-line settings are +`-Zmir-opt-level=0 -Zmir-preserve-ub`. The latter also implies level 0 and keeps +place mentions and reads in trivial switches that could expose UB. These are +[Miri's own defaults](https://github.com/rust-lang/miri/blob/master/src/lib.rs). +Their presence in our driver is established by source inspection. Their adequacy +for our supported fragment still needs the pinned-path review and source-level +negative controls; they are not a formal source-to-MIR correspondence theorem. + +The name `optimized_mir` describes a query/stage, not proof that optional +optimizations ran. A body obtained through that query under the reviewed +preservation configuration may be admissible. Require the reviewed production +pipeline instead of banning the query. Reject unreviewed pass overrides, +borrow-checker bypasses, custom MIR, or extraction settings that circumvent that +pipeline. Validate effective inputs, including environment, Cargo/Charon +configuration files, and build-script output; checking our shell arguments +alone is insufficient. Record permitted semantic variations such as overflow +checking as part of the verified Rust configuration. + +Preservation is not instrumentation that proves access safety. The same driver +explicitly disables rustc's `CheckAlignment` and `CheckNull` MIR passes. +Supported access operations must have their own modeled guards; do not expect +the compiler to insert all the checks needed by a safety proof. + +The configuration must apply when each analyzed crate's MIR is produced. +Current flags cannot undo transformations in precompiled dependency or sysroot +MIR. Charon forces Cargo to rerun workspace extraction, but this does not attest +to every cached dependency's build history. Use a dedicated dependency cache +whose identity includes the controlled pipeline and relevant build inputs, +and whose entries originate from that pipeline. Reuse it only under that +identity. Unknown or externally supplied entries must be rebuilt or rejected. +Directory names and current compiler flags are not evidence of an old entry's +origin. Global initializers, promoted bodies, and CTFE inputs follow the same +origin rule; being called a constant supplies no exemption. + +Do not require a new per-body stage export when the reviewed configuration and +artifact origin cover both the requested query and its fallback. If review +finds a relevant erasure that distinguishes those paths, reject that case or +preserve that specific distinction in Charon. A provenance sidecar, if needed, +must be bound to the exact artifact and incorporated into the same manifest. +This conditional extension does not require another complete AST export. + +Selecting an earlier stage or using the preservation flags does not prove that +all preceding passes preserved UB-producing prefixes. Review the pinned path +and retain that specific correspondence premise. Any newly discovered erasure +requires rejection, a suitable earlier observation, or a justified replacement. + +Charon's existing normalizations remain trusted, with their exact options +recorded. Initially exclude whole features whose normalization hides effects +we cannot justify, especially allocation and custom allocators. If later support +needs information removed by allocator/trait normalization, preserve that +specific information or change that option. Do not guess the original meaning +from the lowered type or a missing field. + +## One exhaustive admission traversal + +Parse the pinned schema strictly. Require the successful extraction marker, +resolve every referenced ID, and reject missing/error bodies, unknown operation +forms, semantic flags, and unsupported declaration metadata. Known diagnostic +metadata may be ignored. A schema or pin change requires explicit review; +warnings and partial extraction cannot yield admission. + +Traverse all discovered roots to a fixed point. Cycles are ordinary recursion, +not a reason to stop examining a body. Inspect a generic body under its declared +parameters; preserve concrete Rust instantiations at call and external-model +boundaries. An erased Lean type or a visited function name alone is not the +identity of an instantiated Rust primitive. + +For each body, visit nested blocks, both branch arms, loop bodies, operands, +places and all projections, embedded constants, normal calls, and every unwind +block. Do not rely on source-level `unsafe` markers or prove reachability to +skip unsupported syntax in the first implementation. A conservative rejection +is easier to review than a second optimizer in the checker. + +The closure includes callable dependencies, globals and their initializers, +promoted computations, and destruction. Referenced type declarations supply +fields, representation/layout metadata, and implicit-effect information. A +reference to a trait dictionary is not itself execution of every dictionary +method; resolve the method at each possible invocation. Dictionary construction +must nevertheless be checked for any actual construction effects. + +Initially permit only calls with a known implementation or an exactly registered +external interpretation. Reject unresolved generic trait calls, function-pointer +calls, unknown callbacks, dynamic dispatch, and escaping borrow reconstruction. +An unannotated ordinary callee can be analyzed; it need not gain a separate +specification. A spec proves its root's behavior through the complete model. + +The mathematical `RustModel` dictionaries are interpretations of values. They +are not contracts for arbitrary Rust trait methods and do not establish that +a Rust type has no destructor. Keep these two uses of dictionaries distinct. + +## Operation rules for the first supported subset + +Start with deterministic integer and initialized-byte computations, ordinary +logical data, and the existing reviewed value-and-borrow subset. The following +rules are release conditions, not exemptions that are already implemented. + +| Operation or feature | Admission rule | +| --- | --- | +| Scalar arithmetic, casts, bounds checks, and byte order | Admit only reviewed type/width/mode combinations and their actual backend implementations. A UB overflow mode cannot silently become wrapping arithmetic. | +| Copy, move, assignment, arguments, and returns | Interpret logical values only when the state relation justifies erasing physical transfer effects. Exact general typed storage is excluded. | +| Creation of values from storage or unchecked construction | Require a guarded producer interpretation before the typed carrier is entered. Invalid production remains forbidden even if its value is unused. | +| `PlaceMention` and projected place formation | Reject unless a reviewed rule proves the projections valid in related states. A count of reference/field projections or absence of raw pointers is insufficient. | +| Residual `Drop`, including conditional and unwind drops | Reject initially. `-eval-drops` does not execute the destructor. Enabling it is not admission. | +| `#[target_feature]`, dispatch variants, unsupported ABIs | Reject initially. Later support must require the real platform/ABI conditions at the call boundary. | +| Raw pointers, unions, raw-memory constants, transmutation, FFI, assembly | Reject unless a specifically admitted primitive completely interprets the operation; no generic successful placeholder. | +| Allocation, allocator parameters, interior mutation, atomics, concurrency | Exclude initially; logical return values alone do not describe their effects. | +| Borrow reconstruction that returns hidden state transformers | Reject until the transformer semantics and state validity are checked. | +| Error or unsupported syntax, missing dependencies | Reject extraction. Never turn a failed analysis into a successful model. | + +Existing value proofs need not be false when these rules reject their extraction +for a stronger claim. In particular, the preserved extraction contains projected +place mentions and numerous opaque dependencies. Each needs a justification; +their presence does not warrant a blanket allowlist. Do not advertise this +design as already admitting all current roots for source-level UB-freedom. + +Charon removes some proven-trivial drops. That removal is part of the reviewed +normalization premise. Do not infer that every generic or opaque type has a +trivial destructor just because no destructor body was imported. A future drop +implementation must extract precise drop glue, inspect its callees and unwind +paths, and preserve conditional/uninitialized/packed-place semantics. + +The source state relation must justify ordinary reference dereferences, +reborrows, retagging, and field projections. For the restricted safe-borrow +subset, this can use the existing borrow semantics and explicit caller frame +premises. Introducing a pointer-producing primitive expands that obligation; +it must not inherit approval just because its output lowers to the same logical +referent type. Unsupported reference validity or interference rules remain +rejections rather than implicit assumptions that every access is safe. + +## Failure, unwind, and divergence + +The existing total and partial contract predicates reject every failure. The +downstream `.fail .undef` marker additionally records forbidden or unsupported +execution. Sequencing preserves failure even when a continuation discards its +argument or diverges; the current Lean tests establish this fact. + +The pinned translator collapses some source UB and panic branches into the +same failure. That is conservative for today's failure-rejecting contracts, +provided the branch is retained. It does not justify panic-tolerant contracts. +Keep panic catching, failure recovery, thread spawning, callbacks with unknown +effects, and panic-tolerant specifications unsupported in this policy. + +Inspect unwind blocks even though Aeneas ignores them. A structural rule can +admit a simple exceptional suffix only when it is entered exclusively after an +already-modeled failure, cannot reenter normal execution, and contains no +unclassified effects. Existing proofs exclude that failure on admitted inputs. +`UnwindResume` in such a suffix is not the same as permitting it on a normal +execution path. Residual destruction remains rejected there as elsewhere. +If the rule cannot establish the connection to modeled failure, reject it. + +An external interpretation cannot return `.div` as a placeholder for unsupported +behavior. A partial contract would then accept it. Its correspondence must +establish that divergence represents only safe infinite execution prefixes. +For example, UB followed by an infinite loop is forbidden, not divergence. +Returning `.undef` for a known unsupported case fails closed; classifying that +case as divergence does not. + +Follow complete compiled execution dependencies, including opaque helper bodies. +Retain the existing rejection of downstream `Option.ofResult` and other +unapproved recovery definitions. Stop only at the actual pinned backend modules, +whose implementations have been reviewed for the admitted operations. Namespace +spelling must not let downstream code impersonate those modules. + +The current backend-boundary audit alone is insufficient for broader safety +claims: review the specific builtins reached by admitted operations, including +their failure conversions and extraction metadata. Calling a builtin +infallible can cause Aeneas to erase it before any Lean dependency audit. The +input admission rules must exclude that builtin or justify the classification. + +The adapter blacklist is a regression check, not a complete proof that failure +cannot be erased. An author could write the same recovery with a direct match +on `Result`. Close that gap through ownership and complete primitive laws: +application execution definitions must come from the unchanged admitted +extraction or a registered interpretation with its checked whole-domain law. +The pinned execution combinators they use also require review, including their +failure behavior; a backend namespace alone supplies no exemption. Arbitrary +handwritten execution helpers do not gain admission merely by passing the axiom +audit. Helpers inside a registered interpretation are covered by that +interpretation's complete law. +Do not attempt to recognize every possible failure-erasing program by name. + +Apply this ownership rule to definitions that determine the executable model. +Ordinary proof lemmas remain ordinary Lean code, subject to the existing proof +and axiom checks. Mathematical decoders also retain their existing role of +defining a contract's domain and observations. Neither a proof helper nor a +decoder may replace the generated execution or turn an unsafe primitive's guard +into an optional library-admission check. + +## External interpretations are explicit trust boundaries + +For each admitted primitive, record its Rust definition identity, crate/source +identity, complete signature and generic arguments, supported instantiations, +target/ABI assumptions, Lean implementation, and relevant extraction settings. +Specify its successful behavior, its safety guard, its failure behavior, and +whether it can affect state. Bind it through the existing ownership manifest. + +An unsupported callee can become such a boundary; it need not remain rejected +forever. Register the exact Rust item and the Lean interpretation, then derive +the precise Charon `--opaque` selection from that registration. Opaqueness +retains the callable declaration and its signature while omitting the body. +Do not exclude the call or turn it into a successful placeholder. An opaque +declaration without an approved interpretation remains an error. This applies +to locally defined unsafe helpers as well as standard-library operations. + +The registration must identify the actual replacement selected by Aeneas, +including its failure classification. A guarded unsafe operation must remain +capable of failure, even when its result is unused. Keep argument evaluation, +original parameters, returned values, and explicit updated states. The chosen +signature and carriers must contain enough information to state its safety +conditions and effects. Opaqueness does not repair a carrier that has already +forgotten a pointer's address, provenance, or relevant storage state. If that +information cannot be supplied by the admitted interface, reject the boundary +until its interface has an adequate interpretation. + +Prefer an ordinary Lean definition with an explicit guard and forbidden branch. +It is axiomatic with respect to Rust: correspondence to the omitted Rust body +is a trusted premise, even though Lean can prove facts about the supplied +definition without adding a logical axiom. The existing unchecked-arithmetic +models use this form. Supporting a literal Lean axiom or an axiomatized behavior +law would additionally require an exact, reviewed extension of the compiled +axiom policy. Never admit arbitrary axioms or a blanket axiom asserting an +inline specification. An inconsistent logical axiom can prove anything; the +guard mechanism cannot repair that inconsistency. + +Report a substituted Rust item as a trusted interpretation, including when it +also owns an inline specification. Proving that specification about the Lean +interpretation does not prove correspondence to the omitted body. A local +substitution should also be visible at its Rust declaration so a source reader +can distinguish an assumed boundary from an analyzed implementation; its exact +annotation syntax remains to be designed. As support grows, the same boundary +can be replaced by an analyzed body without changing callers' contracts. + +For example, admitting `usize::unchecked_add` requires the selected Rust +definition and word width, the exact Lean external definition, the guard +`left.val + right.val ≤ Usize.max`, the exact sum on the good branch, and +`.fail .undef` on the bad branch. Its extraction classification must permit +failure and preserve argument evaluation. It cannot be classified as infallible +merely because a caller is supposed to establish the guard: doing that could +erase an unused call before the caller's proof ever sees its obligation. + +Do not register by an unqualified name, broad path wildcard, or Lean signature +alone. Distinct Rust types can erase to the same Lean type, particularly around +ABI reads. Trait implementation identity and Rust type instantiation remain +relevant even when the emitted function signature looks identical. + +Recording the identities is necessary but not sufficient. If two Rust +instantiations need different ABI or safety observations but the model maps +both to one indistinguishable observation, reject that combination or supply +separately justified data parameters. The existing `Type → Usize` layout input +must not silently identify incompatible Rust instantiations merely because +their Lean carriers coincide. Documented correspondence premises must be +realizable for the claimed instantiations, rather than contradictory premises +that make a contract vacuously true. + +Use the existing complete-definition check for simple guarded primitives such +as unchecked addition and multiplication. A theorem about successful inputs +alone cannot detect a changed implementation on bad inputs. Check the complete +guarded definition, including its failure tag, against an independently stated +expected interpretation. A more complex primitive needs an appropriate checked +semantic law over its whole modeled domain, not just its useful branch. + +Such a check proves that the supplied Lean interpretation is the one intended +by the policy. It does not prove that Rust implements it. That correspondence +remains reviewed and documented. Primitive code, correspondence premises, and +policy changes therefore require review as verification infrastructure, even +when application reviewers primarily read `.rs` specifications. + +Do not import stateful or nondeterministic operations into deterministic pure +models. Aeneas can merge repeated calls and eliminate computations classified +as infallible. Future stateful support must make state/effects explicit and +justify the applicable transformations before being admitted. A hidden global +effect is not made harmless by returning `()`. + +## Bit validity and padding + +For a byte-producing pilot, the storage carrier records initialized payload +bytes. An operation that produces a Rust `T` first checks access conditions +and decodes storage according to `T`'s bit-validity rules. Only success may +produce a value in the extracted typed carrier. A decoder for `bool`, for +example, rejects bytes other than `0` and `1` before creating Lean `Bool`. + +That guard must be part of the primitive's execution, not a `requires` clause +silently added after the invalid production has happened. The caller's proof +must establish it or the primitive fails. Check the result even when discarded, +before a mathematical projection, or before divergence. Later library-model +decoding can impose further requirements on an already-bit-valid value. + +Until typed-copy effects are supported, forget all padding contents and +initializedness. A padding write still evaluates its arguments and satisfies +write-access conditions; it cannot establish retained storage information. +Reject later reads, wider reinterpretations, hashing, byte comparison, and +other observations that rely on forgotten bytes. Mask padding at every boundary +that could expose it, not just typed copies. Initially prefer padding-free +storage such as `MaybeUninit<[u8; N]>`; its eventual interpretation still needs +initialization and access guards. + + + +The mathematical field decoder remains free to choose a coarse abstraction. +The execution state relation, storage primitives, and operation contracts must +retain whatever information safety and the written observations require. This +does not require mathematical models to have canonical raw representatives. + +## Tests that must fail for the right reason + +The following are design witnesses for future controls, not tests already run. +Use real source-to-LLBC-to-Lean examples as well as small checker fixtures. +Separate admission rejection, extraction rejection, and proof rejection in +diagnostics; only an elaborating bad model challenges a Lean proof boundary. + +| Deliberate violation | Required result | +| --- | --- | +| UB-producing call whose result is discarded | Failure remains; `ensures _ => True` cannot be proved. | +| UB-producing call followed by an infinite loop | Partial correctness cannot classify the execution as acceptable divergence. | +| Invalid boolean/nonzero production, followed by dropping the value | Producer guard rejects before entering the typed carrier. | +| Destructor containing a forbidden operation, including generic or unwind drop | Admission rejects residual drop; eventual supported drop exposes the failure. | +| Invalid projected place with otherwise constant return | Admission rejects the unproved projection rule. | +| Unsafe callee hidden by trait dispatch or a callback | Resolve and inspect the real callee, or reject the call. | +| CPU-feature-dependent callee with an innocuous body | Admission rejects missing platform support. | +| Changed Rust type instantiation with the same Lean carrier | Primitive identity/instantiation check rejects mismatched interpretation. | +| Unapproved MIR configuration or a precompiled body that hides an unsafe branch | Configuration/body provenance rejects it; a final AST scan alone must not count as success. | +| Pass override, custom MIR, or borrow-checker bypass supplied through another configuration input | Effective-input policy rejects it even though the driver still sets MIR optimization level 0. | +| Old dependency artifact placed in an otherwise correctly named build cache | Unknown production origin prevents admission until rebuilt or justified. | +| Unsafe access with no alignment/null guard in the model | Admission rejects it; preservation settings and compiler check insertion cannot supply the missing guard. | +| Local opaque helper wrapping failure erasure | Compiled dependency audit rejects it. | +| Handwritten recovery that matches on `Result` without using a blacklisted adapter | Closed execution ownership or the complete primitive law rejects it. | +| Stateful primitive modeled as an infallible pure unit result | Input policy rejects the interpretation before optimizer erasure. | +| Builtin replaces an inspected Rust body with a different execution | Admission checks the actual replacement and its failure classification; inspecting the unused body supplies no approval. | +| Read relying on a previously written padding byte | Storage policy rejects the observation instead of supplying convenient initialized bytes. | +| Missing root, missing dependency, unknown semantic flag, changed LLBC, or stale report | Whole verification run fails. | +| Golden proof passes while live proof fails, or vice versa | Whole verification run fails. | +| Byte/ABI interpretation changed for another target | Configuration identity prevents reuse; new target needs its own correspondence. | + +## Implementation order and remaining obligations + +1. Extend the existing LLBC preflight with one strict traversal, closed schema + handling, root/dependency resolution, source diagnostics, and an admission + report. Add rejection fixtures from the operation inventory. This improves + coverage without yet asserting source-level memory safety. +2. Validate Charon's existing MIR preservation setup and enforce controlled + build origins and effective inputs. Use reviewed interpretations for external + leaves; add earlier-stage evidence only for a concrete unresolved erasure. + Close the compiler/importer correspondence for the restricted fragment. + Review normalization and the reached backend mappings. Resolve projected-place and reference rules before + accepting them; reject unresolved cases, even in current roots. +3. Integrate the mandatory report with the existing two proof builds and final + completion path. Add freshness and skip controls. Maintain a single policy + for all discovered roots in that run. +4. Add guarded bit-validity producers for a small padding-free byte subset, + with complete-definition checks and source-level negative controls. Expand + storage, destruction, state, or concurrency only with their missing semantics. + +Release of a source-level safety claim is blocked until the MIR provenance, +restricted correspondence, operation rules, primitive interpretations, and +mandatory CI path are all supplied. A checker prototype that merely scans +final LLBC must continue to report the existing conditional functional claim. + +This design narrows the accepted language to avoid known gaps; it does not +formally verify rustc, Charon, Aeneas, or the checker. Removing those trusted +premises would require verified translations or kernel-checked certificates. +The practical guarantee is conditional on a finite, explicit trusted boundary, +with no known unsupported operation silently accepted within that boundary. diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md index f7c17a8420..b5bbf8f2ee 100644 --- a/verification/aeneas/DESIGN.md +++ b/verification/aeneas/DESIGN.md @@ -198,6 +198,10 @@ and specifications for review. Both builds regenerate them and require exact source equality. These snapshots are outputs, never inputs to the proof builds; Rust comments remain authoritative and editable Lean projections stay separate. +CI's verification command requires live admission evidence in both builds and +exact copies of the checkout's authored proof sources before and after checking; +development-only bindings remain restricted to the editor's checking command. + All authored Lean packages are rebuilt, including the shared Rust mathematics and its Aeneas companion. Only installed toolchain dependencies may retain compiled caches across verification. An axiom audit of a cached theorem cannot @@ -319,6 +323,20 @@ the library already models every part of Rust's abstract machine. with explicit errors. Add semantics and admission checks before accepting them. Stateful or nondeterministic APIs may need observable traces and effects, rather than only result contracts. +- **Abstract storage and bit validity.** Check byte-to-value production before + entering Aeneas's typed value domain; rejection must remain a forbidden + execution, independently of ordinary library-model admission. A storage model + must account for the translation's omissions as well as its primitives. The + [pinned lowering audit](LOWERING_AUDIT.md) records known omissions and the + additional admission checks needed before making memory-safety claims. + [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the proposed closed + dependency traversal, controlled build origins using Charon's existing MIR + preservation setup, primitive rules, and mandatory CI path. These additional + checks are not implemented yet. + - **Anneal's stronger guarantees.** Construction/mutation closure, universal caller admission, memory validity, provenance, aliasing, and UB-freedom belong to a separately stated stronger claim. Conditional functional proofs can feed diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md new file mode 100644 index 0000000000..130b078e75 --- /dev/null +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -0,0 +1,369 @@ +# Lowering audit before adding memory-safety claims + +This audit records what the pinned extraction retains, forgets, and rejects. +It answers a specific question: could a proof of the generated function omit a +Rust operation that matters to a proposed bit-validity or memory-safety claim? +Yes. Successful extraction and a kernel-checked proof are insufficient unless +the translation preserves the observations needed by that claim. + +The current integration proves conditional functional contracts under the +correspondence premises in [SEMANTICS.md](SEMANTICS.md). It does not yet implement +an abstract storage model or establish general Rust UB-freedom. +[ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) describes the implemented admission +checks on the preserved pre-transformation snapshot and final LLBC, as well as +the additional requirements for future storage and handler models. Those checks +restrict which executions we admit; they do not prove the translator premises +recorded in this audit. + +## Scope and evidence + +The audit used the revisions selected by `anneal/flake.lock` on 2026-10-08: + +- Aeneas: `ca282ec2312a96f6a985a4d23a663690816d3f3e`. +- Charon: `cf02e3f228f97ee7be3a415be56989053063326d`. + +The fetched Aeneas archive's SHA-256 matched the installed build's recorded +source SHA-256. The local Aeneas patch exposes the tuple-newtype option; it does +not change the effect handling examined here. A separate Charon patch saves the +imported AST before transformation and refuses optimized-MIR fallback for local +bodies during admission. The driver uses Charon's Aeneas +preset, `--sysroot default`, and strict error handling. It does not enable +precise/desugared drops or Aeneas's `-feature-gates` option. + +The enumeration below covers every constructor of the pinned LLBC statement +and rvalue languages and lists their auxiliary operation forms. The audit also +examined the MIR importer, the transformation pass lists, the relevant erasing +handlers, builtin replacement policy, and selected effect-removing optimizations. +It is not a proof of every pass, builtin, rustc transformation, or supported +combination of constructs. No end-to-end counterexample was executed. Statements +about ignored operations are findings from the pinned source; their consequences +for future memory claims are deductions from those findings. + +## Confirmed boundaries + +1. **Typed transfers do not retain a storage event.** Copying and moving operate + on logical values. Aeneas tracks moves, uninitialized logical values, and + loans internally, but the pure output does not retain byte initialization, + padding, or provenance. A carrier that treats `MaybeUninit` as an exact + byte sequence could therefore promise more than the lowering preserves. + [Issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405) tracks typed + copies. A restricted storage abstraction can forget all padding contents and + initialization facts, provided supported operations cannot recover them. + Arguments and write-access obligations still need evaluation; forgetting a + padding write does not excuse an invalid access. See [operand evaluation] and + [type translation]. +2. **Residual destructors are ignored by default.** The statement interpreter + treats `Drop` as a no-op. `-eval-drops` instead invalidates the logical value + and processes loans; it does not execute the supplied destructor body. + Charon can make destruction explicit with precise drops and calls to drop + glue, but the current preset does not enable that path. Any safety extension + must account for destruction, including generic and unwind destruction, or + exclude it. Merely turning on `-eval-drops` would not solve this problem. See + [statement interpretation], [drop configuration], and [Charon options]. +3. **Place validity can be omitted.** Charon documents that `PlaceMention` can + cause UB when its projections are invalid. Aeneas explicitly handles it as a + no-op. Other operations may already enforce the necessary conditions for a + particular program, but that needs an argument; this handler does not provide + one. See [statement syntax] and [statement interpretation]. +4. **Some implicit call preconditions are optional.** Aeneas has a pass that + inserts assertions for `#[target_feature]`, but its flag defaults to false + and our driver does not enable it. Rust can require the enabled CPU features + even when the function body otherwise looks harmless. Such functions need + feature admission or rejection before a safety claim. See [feature gates] + and [Rust target-feature rules]. +5. **Generated failure kinds lose distinctions.** Charon distinguishes panic, + UB, and unwind termination. The interpreter turns every `Abort` into the + same symbolic panic node and ignores the failure kind on `Assert`. It also + ignores `on_unwind` blocks when interpreting calls and assertions. Today's + total and partial contracts reject these failures, so this collapse alone + does not make those branches acceptable. Future panic-tolerant rules must + not assume every generated failure represents a recoverable Rust panic. + Our handwritten `.undef` primitives preserve their own failure tags; they + do not repair tags or effects lost earlier. See [statement interpretation]. +6. **Addresses and allocation effects are abstracted away.** References lower + to their referent types and `Box` lowers to `T`; `Box::new` is eliminated. + Charon's preset also hides allocator parameters. Borrow reasoning remains + part of symbolic execution, but the output does not by itself describe + address alignment, allocation identity, resource lifetime, retagging, or + allocator effects. These are deliberate value abstractions, not automatic + memory-safety theorems. See [type translation], [box elimination], and + [Charon options]. +7. **Typed values already assume a representation domain.** Lean `Bool` cannot + contain an invalid Rust boolean, and an enum constructor does not contain an + invalid physical discriminant. Field records omit padding and niche layout. + Producing such values from storage must be checked before entering that + domain. A type decoder used by an ordinary contract cannot retroactively + expose a UB-producing operation erased by translation. Charon's logical + enum discriminants are explicitly distinct from physical stored tags. See + [expression syntax] and [type translation]. +8. **Earlier normalization remains trusted.** Charon requests promoted MIR for + local functions by default, but can fall back to optimized MIR when that + body is unavailable. Its pinned driver already sets MIR optimization level 0, + `mir_preserve_ub`, and `always_encode_mir` for both selected crates and + dependencies compiled through its wrapper. The `optimized_mir` query name + alone therefore does not establish that optional optimizations ran. + Precompiled dependency/sysroot bodies need their own build-origin evidence + or an explicit external interpretation. The driver also disables + `CheckAlignment` and `CheckNull`; preserving an operation does not supply + all of its safety guards. Charon additionally reconstructs arithmetic checks, + indexing, boxes, matches, and control flow. + A downstream primitive cannot restore an effect that disappeared at an + earlier stage. Source-to-model correspondence therefore remains a premise; + checking final LLBC alone cannot establish it. See [MIR configuration], + [MIR selection], and [Charon transformations]. + +These are limitations on stronger claims, not evidence that the current +numerical propositions are false. Conversely, they apply inside annotated +functions too: finding every annotation does not establish that every relevant +operation in its dependency closure was faithfully modeled. + +## Complete LLBC operation inventory + +“Logical” below means the value-and-borrow interpretation. It does not mean +that abstract bytes, physical layout, or all Rust safety conditions are modeled. +“Rejected” means that a surviving unsupported form reaches an error in the +examined handler; strict driver error handling must remain enabled. + +All 18 `StatementKind` constructors appear in this table. See [statement syntax] +and [statement interpretation]. + +| Statement | Disposition relevant to this audit | +| --- | --- | +| `Assign` | Evaluates a logical rvalue and updates a logical place; no general byte-validity production check. | +| `SetDiscriminant` | Updates a logical ADT, not a stored tag or niche encoding. | +| `StorageLive` | Removed in preprocessing or treated as a no-op; no storage allocation event. | +| `StorageDead` | Some removed in preprocessing; remaining ones invalidate a logical value and process loans. | +| `PlaceMention` | Ignored; projection-validity checks need separate justification. | +| `Borrowck` | Removed with compiler-only borrow information. This does not model runtime retagging. | +| `Drop` | Ignored by default; alternative flag handles logical invalidation, not destructor execution. | +| `Assert` | Condition evaluated; failure kind and unwind block ignored. | +| `InlineAsm` | Rejected by the statement handler. | +| `Call` | Translated call retained subject to builtin replacement and later optimization; unwind block ignored. | +| `Abort` | All three kinds become symbolic panic. | +| `Return` | Produces the logical return; physical transfer and implicit cleanup need correspondence. | +| `UnwindResume` | Rejected if interpreted; ignored unwind blocks are not interpreted. | +| `Break` | Structured loop control. | +| `Continue` | Structured loop control. | +| `Nop` | No operation. | +| `Switch` | Logical branch/match interpretation. | +| `Loop` | Symbolic loop interpretation and pure loop/recursive extraction. | + +All 10 `Rvalue` constructors appear below. See [expression syntax] and +[rvalue interpretation]. + +| Rvalue | Disposition relevant to this audit | +| --- | --- | +| `Use` | Evaluates operand; ignores its `WithRetag` flag. | +| `Ref` | Creates symbolic borrows/loans; final reference representation is the referent value. | +| `RawPtr` | Rejected by the rvalue handler. | +| `BinaryOp` | Logical scalar operations; pointer `Offset` rejected. Arithmetic correspondence includes overflow mode. | +| `UnaryOp` | Logical `Not`, `Neg`, and supported casts; unsupported casts rejected. | +| `NullaryOp` | Surviving runtime-check queries rejected by the rvalue handler. | +| `Discriminant` | Reads logical enum variant discriminant, not physical tag bytes. | +| `Aggregate` | Builds logical ADTs/arrays; union construction and raw-pointer aggregates unsupported. | +| `Len` | Requires earlier conversion to a function call; surviving form rejected. | +| `Repeat` | Requires earlier conversion to a function call; surviving form rejected. | + +The auxiliary operation forms are finite too: + +- **Operands:** `Copy`, `Move`, `Const`. Copies retain logical content; moves + invalidate the source in the interpreter. Neither retains a physical transfer + event. Constant normalization is another correspondence boundary. +- **Places:** `Local`, `Global`, `Projection`. Projections are `Deref`, `Field`, + `PtrMetadata`, `Index`, `Subslice`. Raw-pointer dereference is explicitly + rejected; array/slice indexing is converted to calls with logical bounds + checks. Field/dereference reasoning is over logical values. Pointer metadata + is not a provenance or reference-validity certificate. +- **Borrows:** `Shared`, `Mut`, `TwoPhaseMut`, `Shallow`, `UniqueImmutable`. + Shallow borrows are removed by preprocessing; the remaining supported forms + participate in loan reasoning. `WithRetag` is `Yes` or `No`, ignored by `Use`. +- **Casts:** `Scalar`, `RawPtr`, `FnPtr`, `Unsize`, `Transmute`, `Concretize`. + Scalar casts translate numerically. The supported scalar-pointer cast calls a + backend model that always returns `.fail .undef`. Function-pointer casts, + transmutation, and dynamic-trait concretization are rejected. Supported + array-to-slice unsizing remains a logical conversion; it establishes no byte + representation claim. See [cast translation] and [raw-pointer backend]. +- **Binary operations:** `BitXor`, `BitAnd`, `BitOr`, `Eq`, `Lt`, `Le`, `Ne`, + `Ge`, `Gt`, `Add`, `Sub`, `Mul`, `Div`, `Rem`, `AddChecked`, `SubChecked`, + `MulChecked`, `Shl`, `Shr`, `Offset`, `Cmp`. Overflow modes are `Panic`, `UB`, + `Wrap`; retaining a mode in an intermediate AST is not evidence that every + backend preserves its failure classification. `Offset` is rejected. This + audit did not prove all scalar implementations or their mode combinations. +- **Unary operations:** `Not`, `Neg`, `Cast`. **Nullary operations:** + `UbChecks`, `OverflowChecks`, `ContractChecks`. +- **Abort kinds:** `Panic`, `UndefinedBehavior`, `UnwindTerminate`, all collapsed + by the statement handler. See [abort syntax]. + +Declarations and constants can introduce effects or erase representations even +when the statement roster stays unchanged. Their complete outer constructor +lists are included to make that boundary explicit: + +- **Types:** `Scalar`, `Array`, `Slice`, `Adt`, `Ref`, `RawPtr`, `FnDef`, + `FnPtr`, `DynTrait`, `Pattern`, `Never`, `TypeVar`, `TraitType`, `PtrMetadata`, + `Error`. Signature translation explicitly rejects unsupported types; raw + pointers have a limited backend carrier. ADT fields, traits, builtin mappings, + attributes, regions, and ABI/layout metadata require review beyond this list. + In particular, erasing reference regions or marker-trait evidence does not + establish arbitrary unsafe callers' ownership obligations. See [type syntax]. +- **Constants:** `Bool`, `Integer`, `Char`, `Float`, `Adt`, `Array`, `Ref`, + `Ptr`, `Str`, `ByteStr`, `FnDef`, `FnPtr`, `PtrNoProvenance`, `TypeId`, + `RawMemory`, `Var`, `Global`, `Call`, `TraitConst`, `VTableRef`, `Discriminant`, + `SizeOf`, `AlignOf`, `OffsetOf`, `Opaque`. Normalization converts many to + ordinary expressions or calls. Surviving raw memory and opaque constants + explicitly fail interpretation. Const evaluation can already have selected + values using the compiler's layout and target assumptions. See [constant syntax]. +- **Bodies:** `Unstructured`, `Structured`, `TargetDispatch`, `Extern`, + `Intrinsic`, `Opaque`, `Missing`, `Error`. Our driver requests structured + bodies for one configuration. External/builtin interpretations are trusted + definitions requiring correspondence, not verified Rust bodies. An opaque + leaf must never receive an unconstrained successful implementation merely to + make extraction work. See [body syntax]. + +## Other transformation boundaries + +The [MIR importer] has an exhaustive match over its pinned MIR statement and +terminator forms. Assignments, discriminants, storage markers, calls, assertions, +control flow, drops, assembly and aborts reach the corresponding Charon forms. +`Assume` and `CopyNonOverlapping` become intrinsic calls, not no-ops. Projected +place mentions are retained; mentions of an unprojected local are discarded. +Fake reads and user type ascriptions become borrow-checking information. +Coverage markers, const-evaluation counters, lint-only drop hints and no-ops +are discarded. False edges/unwinds retain only their real control-flow edge. +Coroutine drop, tail calls and yield are explicitly unsupported. This inventory +does not audit the earlier rustc passes that produced the input MIR. + +[Charon transformations] replace explicit overflow, division and bounds checks +with operations that must implement those checks; reconstruct vector/box +operations; convert indexing to calls; and simplify control flow and constants. +It is necessary to inspect the replacement operation, not just note that a check +disappeared. For example, removing an unused unit local is restricted to avoid +removing a read through a pointer. Aeneas preprocessing additionally removes +shallow borrows and storage/borrow-checking markers, erases body regions, and +normalizes unreachable calls and panics. See [Aeneas preprocessing]. + +The inspected pure-output optimizations do not simply discard every call whose +result is unused. `filter_useless` preserves a monadic computation unless it +recognizes unconditional success or a narrowly redundant indexing check. That +is useful positive evidence for our failure marker. It still relies on effect +classification and pure deterministic semantics. Duplicate-call elimination +explicitly warns that stateful backward functions would require a change. +Stateful primitives must make state an explicit input/output, or the applicable +transformations must be changed and justified. See [unused-call filtering], +[failure analysis], and [duplicate-call elimination]. + +Builtin replacement is another separate boundary: matching a Rust name to a +Lean implementation can avoid inspecting its Rust body. The scalar, byte-order, +container, allocation and trait replacements therefore need claim-specific +correspondence. This audit examined the replacement policy and key examples, +not every backend implementation. See [builtin replacements]. + +## Inventory of a preserved zerocopy extraction + +The preserved `forbidden-execution-20261008/zerocopy.llbc` artifact has SHA-256 +`62f9b864513a45ffdaeae802021d73cf3802db28d3337acfbd314d12d2136d7a`. +It contains 188 present function declarations: 130 structured and 58 opaque. +This was an inspection of existing evidence, not a fresh extraction or proof run. +The inventory includes dependencies and generated methods; not every declaration +is an independently specified root. + +- No residual `Drop` or `InlineAsm` statements were present, including unwind + blocks. No target-feature attributes were found on the function declarations. +- Normal bodies contained 39 `PlaceMention` statements. Their projection chains + contained 14 reference dereferences and 26 field projections, with no raw + pointer dereference or index/subslice projections. This does not itself prove + their validity; it limits the concrete cases that need justification for this + artifact. +- Normal bodies contained 26 panic aborts and 12 UB aborts. These retain a + failure in the current generated semantics despite losing the failure kind. +- Unwind blocks contained 503 `UnwindResume` statements and eight UB aborts. + Aeneas ignores the enclosing calls'/assertions' unwind paths. Unwind behavior + cannot therefore be inferred from the normal-result proofs. + +These counts are a checkpoint, not an enforced support policy. A future source +change or pin update can change them. Golden comparison plus proofs does not +replace an admission rule for a stronger safety claim. + +## A principled preservation rule + +Confidence requires more than finding every intentional erasure. Choose a +relation between concrete Rust states and abstract modeled states, then establish +that every concrete behavior relevant to the contract is covered by the model. +An omitted operation is acceptable only if it preserves that relation and cannot +hide a forbidden event or a required observation. For safety, reason about traces +up to the first UB event: that event must remain forbidden in the abstraction. +Treating UB as an arbitrary successful result would defeat this purpose. +Even retaining every operation would be insufficient if an operator, branch, +or builtin replacement had the wrong meaning. An erasure inventory is evidence +for the correspondence argument, not a substitute for it. + +This relation concerns execution semantics, not a new mandatory representation +theorem for each mathematical type decoder. A type's mathematical model may +still forget details irrelevant to its operation contracts. The translation must +preserve whatever observations and safety conditions those contracts require. + +For padding, the relation can forget every padding byte's contents and +initialization. A valid padding write or typed transfer can then preserve the +relation without an explicit event. A later supported read cannot manufacture an +initializedness fact that was forgotten. This restriction rejects some sound +programs, as issue #1405 describes, but it does not justify accepting bad ones. + +Total correctness needs an additional progress argument. Infinitely many erased +Rust steps must not appear as a terminating abstract execution. Preserving just +finite successful results would be insufficient. Partial correctness may admit +divergence, but it must still exclude executions that reach UB. + +Aeneas's [borrow-calculus soundness paper] already proves simulations between +its symbolic, borrow-centric and pointer languages. That gives a method and +substantial evidence for its intended subset. It does not establish our proposed +abstract-byte extension or every pass of the pinned Rust-to-Lean implementation. +The ultimate claim is that a proved abstract contract transfers to the concrete +Rust execution under stated input and correspondence premises. + +The smallest practical next step is a claim-specific supported subset: + +1. Inspect the full dependency closure and implicit type/call effects before the + relevant information is erased. This includes destructor-bearing types, + target-feature attributes and external calls, not just explicit `unsafe`. +2. Require an interpretation and correspondence argument for every admitted + effect; reject unsupported cases. Destructors need precise extraction or a + justified exclusion. An LLBC-only check cannot discover an earlier erasure. +3. Keep byte-to-value production behind checked storage primitives. Preserve + forbidden execution through sequencing and any future handlers. Today’s + `.undef` rules cover represented primitives, not arbitrary source operations. +4. Challenge the boundaries with negative controls: invalid production, ignored + results, destruction, invalid place formation, and eventually CPU-feature + and unwind behavior. Differential tests against an abstract-machine + interpreter are useful evidence; they do not prove exhaustive equivalence. + +A verified interpreter or kernel-checked translation certificate could make +this argument compositional and shrink the translator's trusted boundary. +That would be a larger project. Neither this source enumeration nor ordinary +golden/proof checks provide such a certificate. + +[statement syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/bodies/structured.rs +[expression syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/bodies/expressions.rs +[type syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/type_level/types.rs +[constant syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/bodies/values.rs +[body syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/bodies.rs +[abort syntax]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/ast/bodies.rs#L215 +[statement interpretation]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/interp/InterpStatements.ml#L779 +[operand evaluation]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/interp/InterpExpressions.ml#L556 +[rvalue interpretation]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/interp/InterpExpressions.ml#L1464 +[type translation]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/symbolic/SymbolicToPureTypes.ml#L139 +[drop configuration]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/Config.ml#L628 +[feature gates]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/Config.ml#L349 +[Rust target-feature rules]: https://doc.rust-lang.org/reference/attributes/codegen.html#the-target_feature-attribute +[Charon options]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/options.rs#L525 +[MIR configuration]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/bin/charon-driver/driver.rs#L33 +[MIR selection]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/bin/charon-driver/translate/get_mir.rs#L60 +[MIR importer]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/bin/charon-driver/translate/translate_bodies.rs#L1501 +[Charon transformations]: https://github.com/AeneasVerif/charon/blob/cf02e3f228f97ee7be3a415be56989053063326d/charon/src/transform/mod.rs#L105 +[Aeneas preprocessing]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/PrePasses.ml#L2342 +[box elimination]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/pure/PureMicroPassesGeneral.ml#L2156 +[cast translation]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/symbolic/SymbolicToPureExpressions.ml#L560 +[raw-pointer backend]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/backends/lean/Aeneas/Std/RawPtr.lean#L31 +[unused-call filtering]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/pure/PureMicroPassesGeneral.ml#L1157 +[failure analysis]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/pure/PureUtils.ml#L1544 +[duplicate-call elimination]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/pure/PureMicroPassesGeneral.ml#L607 +[builtin replacements]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/extract/ExtractBuiltin.ml#L507 +[borrow-calculus soundness paper]: https://arxiv.org/html/2404.02680v1 diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index aafa31381e..20ca4da81b 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -51,6 +51,13 @@ each tool answers a different question: This is the **extracted model**: executable Lean definitions representing the Rust program. Extraction includes called functions, not just the annotated function's body. + Before Aeneas runs, `admission.py` follows every executable dependency from + every discovered specification in two snapshots: original promoted MIR as + imported by Charon, and final LLBC. Annotation status never exempts a callee. + Unsupported drops, raw pointers, indirect calls, foreign code, and unknown + effects reject extraction. This prevents an operation from being accepted + simply because a later lowering forgets it. The small Charon snapshot patch + preserves evidence; it changes neither Aeneas nor the execution semantics. 3. Our Lean declarations describe how extracted values are interpreted as mathematical values. A `RustModel` supplies a mathematical type and a decoder. Successful decoding defines which representations a contract admits. The @@ -85,7 +92,7 @@ Aeneas also distinguishes execution from the value returned by execution. A successful computation may itself return a Rust `Option` or Rust `Result`. Thus successful execution returning Rust `None`, a decoder rejecting a value, and the function panicking are three different events. Total `spec` requires -success; `partial spec` also allows divergence, while still excluding panic. +success; `partial spec` also allows divergence, while still excluding panic and forbidden execution (`.fail .undef`). The independent comparison checks the specification itself. For an identity function, both `ensures r => True` and `ensures r => r = x` are provable about @@ -101,6 +108,12 @@ differences between them, but each build must prove all the same contracts and pass the same audits. Neither build substitutes the inline mathematical decoder for an extracted function definition. +CI invokes `workspace.py verify`, which requires fresh live-extraction admission +even when checking the golden definitions. It also checks that the copied proof +sources still match the checkout before and after compilation. The editor's +`check` command also supports development bindings, which cannot certify a Rust +extraction. + Each proof check rebuilds the proof package and the shared Lean packages authored in this checkout. Lake may reuse the pinned compiler and dependency artifacts; it must not reuse an earlier compiled meaning of an edited shared model. @@ -144,6 +157,25 @@ checks. This integration proves conditional functional behavior; it does not prove that every caller meets the requirements or that zerocopy's unsafe pointer operations are sound. +## Unsafe boundaries and admission + +`external.json` lists exact reviewed Rust identities and signatures, with the +Lean interpretation used at each boundary. It derives the two local `--opaque` +selections; arbitrary opaque flags are rejected. A changed local helper body +requires a fresh review and an updated body digest. Registration is a trusted +Rust-to-model premise, not a Lean proof of the omitted body. Standard-library +builtin correspondence also remains part of the pinned translator's trust +boundary. See [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) for the implemented +fragment and [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the erasure inventory. + +The binding manifest records both inspected snapshots, their dependency +closures, exact registry identity, sources, compiler configuration, and patched +runtime. Inputs are captured before compilation and checked again during binding +and after proof checking. Neither a stale report nor development-only extraction +qualifies as completed verification. This remains conditional safety for the +admitted fragment under explicit correspondence premises, not a rustc proof or +whole-program unsafe-code certification. + ## Scope and proofs Extraction starts from the function and nominal-type owners of every present diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py new file mode 100644 index 0000000000..ee26720040 --- /dev/null +++ b/verification/aeneas/admission.py @@ -0,0 +1,819 @@ +#!/usr/bin/env python3 +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Reject unreviewed execution before Aeneas can erase its effects. + +This checker admits the pinned value-and-borrow fragment, not arbitrary memory +operations. Its correspondence premises are documented in LOWERING_AUDIT.md. In +particular, valid incoming references and the reviewed borrow translation are +premises; neither is inferred from a list of bytes. Storage-producing operations +are exact registered leaves with guards, rather than unchecked carrier casts. + +The traversal starts at every bound specification. Annotation status never +exempts a callee. Unknown constructors, indirect calls, drops, and raw storage +observations fail closed. The report identifies the inspected LLBC and selected +interpretations; it is evidence of this inspection, not a proof of rustc. +""" + +import argparse +import hashlib +import json +import os +import re +from pathlib import Path + +import source_inventory + + +# These provided methods require memory or I/O semantics outside our admitted +# fragment. Their unused signatures must not pull that fragment into a bound +# which only consumes IntoBytes's law. The patched compiler rejects every +# resolved reference to an excluded provided method; exclusion never supplies +# an opaque implementation or a theorem about its behavior. Required trait +# methods, bounds, associated constraints, and original method slots remain. +EXCLUDED_PROVIDED_METHODS = tuple('zerocopy::IntoBytes::' + name for name in ( + 'as_bytes', 'as_mut_bytes', 'write_to', 'write_to_prefix', 'write_to_suffix', + 'as_bytes_mut')) + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def untag(value): + # Disable serialization sharing in the extraction command. Different AST + # domains reuse deduplication indices; guessing their domain is unsafe. + if isinstance(value, dict) and set(value) == {'Untagged'}: + return value['Untagged'] + return value + + +def variant(value): + value = untag(value) + if isinstance(value, str): + return value, None + if isinstance(value, dict) and len(value) == 1: + return next(iter(value.items())) + raise ValueError(f'Invalid LLBC variant: {value!r}') + + +def fields(value, expected): + if not isinstance(value, dict) or set(value) != set(expected.split()): + raise ValueError(f'Unreviewed LLBC fields: expected {expected}, got {value!r}') + + +class Admission: + def __init__(self, data, registry): + if data.get('has_errors') is not False or data.get('charon_version') != '0.1.276': + raise ValueError('Admission requires successful LLBC from the reviewed Charon schema') + self.crate = data['translated'] + self.functions = {f['def_id']: f for f in self.crate['fun_decls'] if f} + self.types = {t['def_id']: t for t in self.crate['type_decls'] if t} + self.registry = registry + self.visited = {} + self.calls = [] + self.globals = set() + self.current = None + self.locals = {} + self.checked_types = set() + options = self.crate['options'] + targets = self.crate['target_information'] + if (len(targets) != 1 or targets[0]['value']['target_pointer_size'] != 8 or + targets[0]['value']['is_little_endian'] is not True): + raise ValueError('Admission currently requires a little-endian 64-bit target') + # Review the whole option profile. A new Charon flag must not silently + # enable an erasure just because the old subset of flags still matches. + required = dict.fromkeys("""ullbc precise_drops monomorphize + start_from_pub extract_opaque_bodies translate_all_methods + eager_vtables duplicate_defaulted_methods no_doc_comments + remove_unused_clauses desugar_drops resugar_drops detect_drop_flags + raw_consts unsized_strings print_original_ullbc print_ullbc + print_built_llbc print_llbc print_layouts no_serialize skip_borrowck + erase_body_lifetimes no_typecheck no_normalize no_reorder_decls + no_compute_layout_guarantees""".split(), False) + required.update(dict.fromkeys("""hide_marker_traits hide_allocator + remove_unused_self_clauses remove_adt_clauses ops_to_function_calls + index_to_function_calls treat_box_as_builtin no_gen_tuple_structs + reconstruct_fallible_operations reconstruct_asserts + reconstruct_matches deallocate_all_locals unbind_item_vars + no_dedup_serialized_ast abort_on_error error_on_warnings""".split(), True)) + required.update(dict.fromkeys("""rustc_args targets start_from_if_exists + start_from_attribute include exclude""".split(), [])) + required['exclude'] = list(EXCLUDED_PROVIDED_METHODS) + required.update(dict.fromkeys('monomorphize_mut consts dest_dir format'.split(), None)) + required.update(preset='Aeneas', mir='Promoted', sysroot='default', + lift_associated_types=['*']) + if set(options) != set(required) | {'start_from', 'opaque', 'dest_file'}: + raise ValueError('Unreviewed extraction option fields') + for key, expected in required.items(): + if options[key] != expected: + raise ValueError(f'Unreviewed extraction option {key}: {options[key]!r}') + stages = {variant(f['body'])[0] for f in self.functions.values() + if f['body'] != 'Opaque'} + if len(stages) != 1 or not stages <= {'Unstructured', 'Structured'}: + raise ValueError('Missing or mixed admission body stages') + self.before = stages == {'Unstructured'} + # Opaque selection comes only from the registry, never from arbitrary + # command-line flags which could hide an unsafe local body. + expected = sorted(row['rust'] for row in registry if row.get('opaque')) + if sorted(options['opaque']) != expected: + raise ValueError('Opaque selections disagree with the external interpretation registry') + + def name(self, name): + parts = [] + for element in name: + tag, body = variant(element) + if tag == 'Ident' and body[1] == 0: + parts.append(body[0]) + elif tag == 'Impl': + if 'Ty' in body: + parts.append('{' + self.ty_name(body['Ty']['skip_binder']) + '}') + elif 'Trait' in body: + # Preserve the exact trait implementation identity in the + # signature fingerprint below; display is only a lookup key. + impl = self.crate['trait_impls'][body['Trait']]['impl_trait'] + trait = self.crate['trait_decls'][impl['id']] + args = impl['generics']['types'] + parts.append('{' + self.name(trait['item_meta']['name']) + + '<' + ','.join(self.ty_name(t) for t in args) + '>}') + else: + raise ValueError('Unknown implementation identity') + elif tag == 'Builtin' and isinstance(body[0], dict) and set(body[0]) == {'Tuple'}: + parts.append('tuple' + str(body[0]['Tuple'])) + elif tag == 'Builtin' and body == ['Str', 0]: + parts.append('str') + else: + raise ValueError(f'Unknown Rust identity component: {element}') + return '::'.join(parts) + + def ty_name(self, ty): + tag, body = variant(ty) + if tag == 'Never': + return '!' + if tag == 'Scalar': + if body == 'Bool': + return 'bool' + if isinstance(body, dict) and set(body) == {'Integer'}: + signedness, width = variant(body['Integer']) + if signedness not in {'Signed', 'Unsigned'} or width not in { + 'I8', 'I16', 'I32', 'I64', 'I128', 'Isize', + 'U8', 'U16', 'U32', 'U64', 'U128', 'Usize'}: + raise ValueError(f'Unreviewed integer {body}') + return width.lower() + raise ValueError(f'Unsupported scalar {body}') + if tag == 'TypeVar': + kind, index = variant(body) + if kind == 'Free': return 'T' + str(index) + if kind == 'Bound' and index[0] == 0: return 'T' + str(index[1]) + raise ValueError(f'Unreviewed type variable {body}') + if tag == 'Adt': + base = self.name(self.types[body['id']]['item_meta']['name']) + args = body['generics']['types'] + if body['generics']['const_generics']: + raise ValueError('Nominal const-generic value carriers are unsupported') + self.check_type(body['id']) + return base + ('<' + ','.join(self.ty_name(x) for x in args) + '>' if args else '') + if tag in {'Slice', 'Array'}: + suffix = '' if tag == 'Slice' else ';' + self.const_name(body[1]) + return '[' + self.ty_name(body[0]) + suffix + ']' + if tag == 'Ref': + if body[2] not in {'Shared', 'Mut'}: + raise ValueError('Unreviewed reference mutability') + return ('&mut ' if body[2] == 'Mut' else '&') + self.ty_name(body[1]) + raise ValueError(f'Unreviewed type {tag}; raw pointers and storage are not logical values') + + def const_name(self, value): + value, _ = untag(value) + tag, body = variant(value) + if tag == 'Var': + kind, index = variant(body) + if kind == 'Free': return 'N' + str(index) + if kind == 'Bound' and index[0] == 0: return 'N' + str(index[1]) + raise ValueError(f'Unreviewed const variable {body}') + if tag == 'Integer': + return next(iter(body.values()))[1] + raise ValueError(f'Unreviewed const-generic expression {tag}') + + def check_type(self, index): + if index in self.checked_types: + return + self.checked_types.add(index) + declaration = self.types[index] + kind, body = variant(declaration['kind']) + name = self.name(declaration['item_meta']['name']) + if kind == 'Opaque': + if name not in {'tuple0', 'str', 'core::fmt::Arguments', + 'core::fmt::Formatter', 'core::marker::PhantomData', + 'core::num::nonzero::NonZero', + 'core::num::niche_types::NonZeroUsizeInner'}: + raise ValueError(f'Unreviewed opaque value carrier {name}') + return + if kind == 'Struct': + children = body + elif kind == 'Enum': + children = [field for case in body for field in case['fields']] + else: + raise ValueError(f'Unreviewed value carrier {kind}: {name}') + for field in children: + self.ty_name(field['ty']) + + def prototype(self, function): + sig = function['signature'] + fields(sig, 'is_unsafe abi is_variadic inputs output') + if sig['abi'] != 'Rust' or sig['is_variadic']: + raise ValueError('Unsupported ABI or variadic function') + return {'unsafe': sig['is_unsafe'], + 'inputs': [self.ty_name(x) for x in sig['inputs']], + 'output': self.ty_name(sig['output']), + 'types': len(function['generics']['types']), + 'consts': len(function['generics']['const_generics'])} + + def visit(self, index): + if index in self.visited: + return + function = self.functions.get(index) + if function is None: + raise ValueError(f'Missing executable dependency {index}') + meta = function['item_meta'] + name = self.name(meta['name']) + prototype = self.prototype(function) + if meta['has_errors'] or meta['is_extern']: + raise ValueError(f'Untranslated or foreign-ABI dependency {name}') + for attribute in meta['attr_info']['attributes']: + kind, detail = variant(attribute) + if kind == 'DocComment': + continue + if kind == 'Builtin': + tag, _ = variant(detail) + if tag in {'Inline', 'TrackCaller'}: + continue + elif kind == 'Unknown': + fields(detail, 'path args') + if detail['path'] in {'allow', 'warn', 'deny', 'forbid', + 'must_use', 'cold', 'deprecated', 'doc', 'cfg', 'cfg_attr'}: + continue + raise ValueError(f'Unreviewed function attribute {kind} on {name}') + matches = [] + for row in self.registry: + selected = row.get('before', row) if self.before else row + if selected['rust'] == name and selected['signature'] == prototype: + matches.append(row) + if matches: + if len(matches) != 1: + raise ValueError(f'External interpretation signature changed: {name}') + # A builtin may replace a visible Rust body. Always select the + # interpretation first, rather than approving the unused body. + self.visited[index] = {'rust': name, 'origin': 'interpretation', + 'lean': matches[0]['lean']} + return + if function['body'] == 'Opaque' or meta['is_local'] is not True: + raise ValueError(f'No reviewed interpretation for {name}') + stage, body = variant(function['body']) + if stage not in {'Structured', 'Unstructured'}: + raise ValueError(f'Unknown body stage {stage}') + fields(body, 'span bound_body_regions locals body comments') + if self.contains_reference(function['signature']['output']): + raise ValueError(f'Escaping borrow is unsupported: {name}') + self.visited[index] = {'rust': name, 'origin': 'body'} + previous = self.current, self.locals + self.current = name + self.locals = {local['index']: local for local in body['locals']['locals']} + for local in self.locals.values(): + self.ty_name(local['ty']) + if local['drop_flag_for'] is not None: + raise ValueError(f'Conditional drop flag in {name}') + try: + if stage == 'Structured': + self.block(body['body']) + else: + self.cfg(body['body']) + except ValueError as error: + raise ValueError(f'{name}: {error}') from error + finally: + self.current, self.locals = previous + + def contains_reference(self, value, seen=None): + seen = set() if seen is None else seen + tag, body = variant(value) + if tag == 'Ref': + return True + if tag in {'Slice', 'Array'}: + return self.contains_reference(body[0], seen) + if tag == 'Adt': + if any(self.contains_reference(t, seen) for t in body['generics']['types']): + return True + index = body['id'] + if index in seen: + return False + seen.add(index) + kind, children = variant(self.types[index]['kind']) + if kind == 'Enum': + children = [field for case in children for field in case['fields']] + if kind in {'Struct', 'Enum'}: + return any(self.contains_reference(field['ty'], seen) for field in children) + return False + + def assertion(self, assertion): + fields(assertion, 'cond expected check_kind') + if type(assertion['expected']) is not bool: + raise ValueError('Unreviewed assertion polarity') + self.operand(assertion['cond']) + check = assertion['check_kind'] + if check is None: + return + tag, detail = variant(check) + if tag == 'BoundsCheck': + fields(detail, 'len index') + operands = list(detail.values()) + elif tag == 'Overflow': + # Charon uses this only for diagnostics; the preceding Boolean + # computation contains the actual arithmetic check. + self.rvalue({'BinaryOp': detail}) + return + elif tag in {'OverflowNeg', 'DivisionByZero', 'RemainderByZero'}: + operands = [detail] + else: + raise ValueError(f'Unreviewed assertion kind {tag}') + for operand in operands: + self.operand(operand) + + def abort(self, abort): + tag, _ = variant(abort) + # The pinned interpreter collapses source UB aborts into panic. Both + # remain rejected by every admitted contract. No recovery or failure + # handler is admitted; adding one requires preserving this distinction. + if tag not in {'Panic', 'UndefinedBehavior'}: + raise ValueError(f'Unreviewed abort {tag}') + + def place(self, place, indexed=False): + fields(place, 'kind ty') + self.ty_name(place['ty']) + tag, body = variant(place['kind']) + if tag == 'Local': + if body not in self.locals: + raise ValueError('Unknown local place') + elif tag == 'Global': + self.global_value(body['id']) + elif tag == 'Projection': + self.place(body[0], indexed) + projection, detail = variant(body[1]) + if projection == 'Deref': + if variant(body[0]['ty'])[0] != 'Ref': + raise ValueError('Dereference without a modeled reference') + elif projection == 'PtrMetadata': + if variant(body[0]['ty'])[0] != 'Ref': + raise ValueError('Metadata without a modeled reference') + elif projection == 'Index' and indexed and self.before: + fields(detail, 'offset from_end') + if detail['from_end'] is not False or variant(body[0]['ty'])[0] not in {'Slice', 'Array'}: + raise ValueError('Unreviewed indexing base or direction') + self.operand(detail['offset']) + elif projection != 'Field': + # Indexing must use a reviewed, guarded builtin. In particular, + # PlaceMention cannot bypass its bounds check by being erased. + raise ValueError(f'Unreviewed place projection {projection}') + else: + raise ValueError(f'Unsupported place {tag}') + + def global_value(self, index): + if index in self.globals: + return + self.globals.add(index) + global_ = self.crate['global_decls'][index] + if global_['global_kind'] != 'NamedConst' or global_['item_meta']['has_errors']: + raise ValueError('Unreviewed static or global origin') + self.constant(global_['value']) + + def operand(self, operand): + tag, body = variant(operand) + if tag in {'Copy', 'Move'}: + self.place(body, indexed=True) + elif tag == 'Const': + self.constant(body) + else: + raise ValueError(f'Unsupported operand {tag}') + + def constant(self, constant): + value, ty = untag(constant) + self.ty_name(ty) + tag, body = variant(value) + if tag == 'Opaque' and body == 'Missing metadata' and self.ty_name(ty) == 'tuple0': + # Original Charon uses this exact unit token for absent thin-pointer + # metadata. It is not a raw value or an unevaluated Rust constant. + return + if tag in {'Bool', 'Integer', 'Str', 'Discriminant'}: + return + if tag == 'Adt': + for field in body[1]: + self.constant(field) + return + if tag == 'Global': + self.global_value(body['id']) + return + if tag == 'Call': + function, args = body + if variant(function['kind'])[0] != 'Fun': + raise ValueError('Unresolved constant producer') + for arg in args: + self.constant(arg) + self.visit(function['kind']['Fun']) + return + if tag == 'TraitConst': + # Resolved dictionaries are traversed below; unresolved constants + # cannot be treated as harmless data because their producer may run. + self.dictionary(body[0]) + return + raise ValueError(f'Unsupported constant {tag}; no raw-memory or CTFE placeholder') + + def dictionary(self, reference): + # The pinned dictionaries explicitly name their implementations. A + # type-variable clause is acceptable only for marker traits with no + # executable methods; never for a callback chosen by a caller. + reference = untag(reference) + kind = reference['kind'] + tag, body = variant(kind) + if tag == 'TraitImpl': + index = body['id'] + impl = self.crate['trait_impls'][index] + for method in impl['methods']: + if method is not None: + self.visit(method['skip_binder']['id']) + elif tag in {'BuiltinOrAuto', 'Clause'}: + trait = self.crate['trait_decls'][reference['trait_decl_ref']['skip_binder']['id']] + if trait['methods']: + raise ValueError(f'Unresolved dictionary with executable methods {tag}') + # Method-free dictionaries supply typed, evaluated constant data. + # Compiler CTFE validity remains an explicit normalization premise. + return + else: + raise ValueError(f'Unresolved executable dictionary {tag}') + + def rvalue(self, rvalue): + tag, body = variant(rvalue) + if tag == 'Use': + self.operand(body[0]) + if body[1] not in {'Yes', 'No'}: + raise ValueError('Unknown retag mode') + elif tag == 'BinaryOp': + op, mode = variant(body[0]) + if op not in {'BitXor', 'BitAnd', 'BitOr', 'Eq', 'Lt', 'Le', 'Ne', 'Ge', 'Gt', + 'Add', 'Sub', 'Mul', 'Div', 'Rem', 'Shl', 'Shr', + 'AddChecked', 'SubChecked', 'MulChecked'}: + raise ValueError(f'Unreviewed binary operation {op}') + if mode == 'UB' and op in {'Add', 'Mul'}: + # Charon resugars these into the exact registered Usize leaves. + # Require both operands to have that carrier; no generic or + # signed unchecked arithmetic inherits this registration. + for operand in body[1:]: + kind, value = variant(operand) + ty = value['ty'] if kind in {'Copy', 'Move'} else untag(value)[1] + if self.ty_name(ty) != 'usize': + raise ValueError('Unsupported unchecked arithmetic carrier') + leaf = 'core::num::{usize}::unchecked_' + op.lower() + if not any(row['rust'] == leaf for row in self.registry): + raise ValueError(f'No reviewed interpretation for {leaf}') + self.calls.append({'caller': self.current, 'callee': leaf, + 'implicit': True}) + elif mode == 'UB' and op in {'Div', 'Rem'}: + # Rust's preceding assertions guard these MIR operations. The + # pinned backend additionally performs the divisor/overflow + # checks; final LLBC must retain checked division/remainder. + for operand in body[1:]: + kind, value = variant(operand) + ty = value['ty'] if kind in {'Copy', 'Move'} else untag(value)[1] + if not re.fullmatch(r'(u|i)(8|16|32|64|128|size)', self.ty_name(ty)): + raise ValueError('Unsupported division/remainder carrier') + elif mode not in {None, 'Panic', 'Wrap'}: + raise ValueError(f'Unreviewed arithmetic mode {mode}; use a guarded primitive') + for operand in body[1:]: + self.operand(operand) + elif tag == 'UnaryOp': + op, detail = variant(body[0]) + if op == 'Cast': + cast, types = variant(detail) + if cast == 'Unsize': + source, target, metadata = [untag(t) for t in types] + if set(source) != {'Ref'} or set(target) != {'Ref'}: + raise ValueError('Only array-reference to slice-reference unsizing is supported') + source, target = source['Ref'], target['Ref'] + if source[2] != target[2] or source[2] not in {'Shared', 'Mut'}: + raise ValueError('Unreviewed unsizing mutability') + source, target = untag(source[1]), untag(target[1]) + if (set(source) != {'Array'} or set(target) != {'Slice'} or + self.ty_name(source['Array'][0]) != self.ty_name(target['Slice'][0])): + raise ValueError('Unreviewed unsizing element or carrier') + if (not isinstance(metadata, dict) or set(metadata) != {'Length'} or + self.const_name(metadata['Length']) != self.const_name(source['Array'][1])): + raise ValueError('Unreviewed unsizing metadata') + elif cast == 'Scalar': + for endpoint in types: + if not (endpoint == 'Bool' or isinstance(endpoint, dict) + and set(endpoint) == {'Integer'}): + raise ValueError(f'Unreviewed scalar cast endpoint {endpoint}') + else: + raise ValueError(f'Unreviewed cast {cast}') + elif op != 'Not' and not (op == 'Neg' and detail in {'Panic', 'Wrap'}): + raise ValueError(f'Unreviewed unary operation {op}') + self.operand(body[1]) + elif tag == 'Aggregate': + kind, _ = variant(body[0]) + if kind not in {'Adt', 'Array'}: + raise ValueError(f'Unreviewed aggregate {kind}') + for operand in body[1]: + self.operand(operand) + elif tag == 'Discriminant': + self.place(body) + elif tag == 'Ref': + fields(body, 'place kind ptr_metadata') + if body['kind'] not in {'Shared', 'Mut', 'TwoPhaseMut', 'Shallow'}: + raise ValueError('Unsupported reference kind') + self.place(body['place'], indexed=True) + if body['ptr_metadata'] is not None: + self.operand(body['ptr_metadata']) + else: + raise ValueError(f'Unreviewed rvalue {tag}') + + def block(self, block, unwind=False): + fields(block, 'span id statements') + for statement in block['statements']: + fields(statement, 'span id kind comments_before') + tag, body = variant(statement['kind']) + if unwind and tag not in {'StorageDead', 'UnwindResume', 'Abort', 'Nop'}: + raise ValueError(f'Unclassified unwind effect {tag}') + if tag in {'StorageLive', 'StorageDead', 'Nop', 'Return', 'Break', 'Continue'}: + continue + if tag == 'UnwindResume': + if not unwind: + raise ValueError('UnwindResume on a normal path') + elif tag == 'Assign': + self.place(body[0]); self.rvalue(body[1]) + elif tag == 'PlaceMention': + self.place(body) + elif tag == 'Borrowck': + kind, place = variant(body) + if kind != 'FakeRead': + raise ValueError(f'Unreviewed borrow-checking statement {kind}') + self.place(place) + elif tag == 'Call': + fields(body, 'call on_unwind') + call = body['call']; fields(call, 'func args dest') + category, fn = variant(call['func']) + if category != 'Regular' or variant(fn['kind'])[0] != 'Fun': + raise ValueError('Unresolved trait, callback, or indirect call') + fields(fn, 'kind generics') + callee = fn['kind']['Fun'] + for operand in call['args']: + self.operand(operand) + self.place(call['dest']) + for ty in fn['generics']['types']: + self.ty_name(ty) + for ref in fn['generics']['trait_refs']: + self.dictionary(ref) + target = self.functions[callee] + name = self.name(target['item_meta']['name']) + if name == 'zerocopy::util::transmute_unchecked': + actual = [self.ty_name(ty) for ty in fn['generics']['types']] + if actual != ['u8', 'bool']: + raise ValueError(f'Unsupported transmute instantiation {actual}') + self.calls.append({'caller': self.current, 'callee': name}) + self.visit(callee) + self.block(body['on_unwind'], True) + elif tag == 'Assert': + fields(body, 'assert on_failure on_unwind') + self.assertion(body['assert']) + self.abort(body['on_failure']) + self.block(body['on_unwind'], True) + elif tag == 'Abort': + self.abort(body) + elif tag == 'Switch': + fields(body, 'data branches') + data = body['data'] + fields(data, 'scrutinee branches fallback') + kind, scrutinee = variant(data['scrutinee']) + if kind == 'Value': + self.operand(scrutinee) + elif kind == 'Discriminant': + self.place(scrutinee) + else: + raise ValueError(f'Unreviewed branch scrutinee {kind}') + for value, index in data['branches']: + self.constant(value) + if not 0 <= index < len(body['branches']): + raise ValueError('Invalid branch target') + if data['fallback'] is not None and not 0 <= data['fallback'] < len(body['branches']): + raise ValueError('Invalid fallback branch') + for branch in body['branches']: + self.block(branch, unwind) + elif tag == 'Loop': + self.block(body, unwind) + else: + raise ValueError(f'Unreviewed statement {tag}; drops, assembly and padding observations are excluded') + + def cfg(self, blocks): + """Inspect every original block, including dead and unwind blocks. + + Charon may later remove a dead block. Inspecting it is conservative and + avoids relying on that pass to distinguish unreachable UB from a lost + effect. Terminators are converted to the same operation checks used for + LLBC; only control-flow edges and bookkeeping get separate treatment. + """ + for block in blocks: + fields(block, 'statements terminator') + for stmt in block['statements']: + fields(stmt, 'span kind comments_before') + self.block({'span': stmt['span'], 'id': 0, + 'statements': [dict(stmt, id=0)]}) + term = block['terminator'] + fields(term, 'span kind comments_before') + tag, body = variant(term['kind']) + if tag in {'Goto', 'Return', 'UnwindResume'}: + continue + if tag == 'Call': + fields(body, 'call target on_unwind') + body = {'call': body['call'], 'on_unwind': + {'span': term['span'], 'id': 0, 'statements': []}} + elif tag == 'Assert': + fields(body, 'assert target on_unwind') + self.assertion(body['assert']) + continue + elif tag == 'Switch': + fields(body, 'data branches') + body = {'data': body['data'], 'branches': [ + {'span': term['span'], 'id': 0, 'statements': []} + for _ in body['branches']]} + elif tag != 'Abort': + raise ValueError(f'Unreviewed original terminator {tag}; ' + 'implicit drops and assembly must remain visible') + self.block({'span': term['span'], 'id': 0, 'statements': [ + dict(term, id=0, kind={tag: body})]}) + + def audit(self, roots): + names = {} + for index, function in self.functions.items(): + meta = function['item_meta'] + if not (meta['is_local'] and meta['started_from']): + continue + parts = meta['name'] + if len(parts) > 1 and 'Impl' in parts[-2]: + impl = parts[-2]['Impl'] + if 'Ty' not in impl: + continue + ty, adt = variant(impl['Ty']['skip_binder']) + if ty != 'Adt': + continue + name = self.name(self.types[adt['id']]['item_meta']['name']) + '::' + parts[-1]['Ident'][0] + else: + name = self.name(parts) + names.setdefault(name, []).append(index) + for root in roots: + matches = names.get(root, []) + if len(matches) != 1: + raise ValueError(f'Missing or ambiguous specification root {root}') + self.visit(matches[0]) + return {'roots': sorted(roots), 'executions': list(self.visited.values()), + 'calls': self.calls} + + +def input_identity(root): + """Bind inspection to source, build configuration, and the patched runtime. + + Compiler overrides could invalidate the preserved-MIR premise even though + Charon's serialized options stay unchanged. Reject them before compiling. + Cargo credential files are never inspected or included in the report. + """ + for name, value in os.environ.items(): + if value and (name in {'RUSTFLAGS', 'CARGO_ENCODED_RUSTFLAGS', + 'CARGO_BUILD_RUSTFLAGS', 'RUSTC', 'RUSTC_WRAPPER', + 'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS'} or + re.fullmatch(r'CARGO_TARGET_.*_RUSTFLAGS', name)): + raise ValueError(f'Unreviewed compiler override {name}') + configs = [] + for base in [root / 'zerocopy', root, *root.parents, + Path(os.environ.get('CARGO_HOME', Path.home() / '.cargo'))]: + for suffix in ('.cargo/config', '.cargo/config.toml', 'Charon.toml'): + path = base / suffix + if path.is_file() and path not in configs: + configs.append(path) + cargo_home = Path(os.environ.get('CARGO_HOME', Path.home() / '.cargo')) + configs.extend(p for p in [cargo_home / 'config', cargo_home / 'config.toml'] + if p.is_file() and p not in configs) + for path in configs: + if path.name == 'Charon.toml': + raise ValueError(f'Extraction configuration must be in run.sh, not {path}') + # Conservative lexical check avoids implementing Cargo's precedence + # rules. Even a dormant override is rejected, rather than guessed safe. + text = '\n'.join(line.split('#', 1)[0] for line in path.read_text().splitlines()) + if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b', text): + raise ValueError(f'Unreviewed Cargo compiler configuration: {path}') + # Discovery and freshness use the same unconditional source inventory. + # Cache-like names under src cannot hide newly added Rust specifications. + paths = set(source_inventory.crate_files(root)) + # Reviewed snapshots are outputs, and --update-goldens may change them + # after the live proof. The driver compares both output families separately; + # their directory names cannot exempt similarly named authored inputs. + for directory in ['verification/aeneas', 'tools/aeneas-inline/src', 'anneal/lean']: + paths.update(p for p in (root / directory).rglob('*') + if p.is_file() and '__pycache__' not in p.parts and '.lake' not in p.parts + and not any(p.is_relative_to(root / 'verification/aeneas' / name) + for name in ('golden', 'projections'))) + paths.update(p for p in [root / 'Cargo.lock', root / 'Cargo.toml', + root / 'zerocopy/Cargo.toml', root / 'zerocopy/Cargo.lock', root / 'zerocopy/build.rs', + root / 'tools/Cargo.lock', root / 'tools/Cargo.toml', root / 'tools/aeneas-inline/Cargo.toml', + root / 'anneal/flake.lock', root / 'anneal/flake.nix'] + if p.is_file()) + combined = hashlib.sha256() + for path in sorted(paths): + combined.update(str(path.relative_to(root)).encode()) + combined.update(path.read_bytes()) + tools = Path(os.environ['AENEAS_TOOLCHAIN_DIR']) + return {'project': combined.hexdigest(), + 'configs': [digest(path) for path in configs], + 'runtime': digest(tools / 'aeneas-build.json')} + + +def inspect(root, work, roots, sources, body_digests=None): + registry_path = root / 'verification/aeneas/external.json' + registry = json.loads(registry_path.read_text()) + reports = {} + for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]: + path = work / filename + if not path.is_file(): + raise ValueError(f'Missing mandatory {stage} admission snapshot: {path}') + checked = Admission(json.loads(path.read_text()), registry) + if checked.before != (stage == 'before'): + raise ValueError(f'Wrong AST stage for mandatory {stage} snapshot') + reports[stage] = checked.audit(roots) + reports[stage]['sha256'] = digest(path) + for entry in registry: + if entry.get('opaque') and any(row['rust'] == entry['rust'] + for row in reports['llbc']['executions']): + observed = (body_digests or {}).get(entry['rust']) + if observed != [entry.get('source_body_sha256')]: + raise ValueError(f'Trusted Rust helper body changed; review its interpretation: {entry["rust"]}') + # Compare the unsafe call boundaries that must survive normalization. + # This is a conservative shape check, not a formal simulation theorem. + from collections import Counter + guarded = {row['rust'] for row in registry + if row.get('opaque') or row['signature']['unsafe']} + def guarded_calls(stage): + return Counter((call['caller'], call['callee']) for call in stage['calls'] + if call['callee'] in guarded) + missing = guarded_calls(reports['before']) - guarded_calls(reports['llbc']) + if missing: + raise ValueError(f'Normalization lost a guarded call boundary: {list(missing)}') + # Capture this identity before compilation, then require it unchanged when + # binding the model. Otherwise an editor could change Rust while Charon was + # running and accidentally associate the old model with the new source. + identity_path = work / 'extraction-inputs.json' + if not identity_path.is_file(): + raise ValueError('Missing pre-compilation input identity') + identity = json.loads(identity_path.read_text()) + if identity != input_identity(root): + raise ValueError('Extraction inputs changed during compilation; regenerate') + # No extra selection roster: every function binding supplies one root. + return {'version': 1, 'stages': reports, + 'registry': digest(registry_path), 'sources': sources, + 'inputs': identity} + + +def check_translation(work, evidence): + text = (work / 'Zerocopy/FunsExternal_Template.lean').read_text() + signatures = { + 'util.transmute_unchecked': + 'axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst', + 'util.copy_unchecked': + 'axiom util.copy_unchecked : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)', + 'core.num.Usize.unchecked_add': + 'axiom core.num.Usize.unchecked_add : Std.Usize → Std.Usize → Result Std.Usize', + 'core.num.Usize.unchecked_mul': + 'axiom core.num.Usize.unchecked_mul : Std.Usize → Std.Usize → Result Std.Usize', + } + normalized = ' '.join(text.split()) + for selected in evidence['stages']['llbc']['executions']: + expected = signatures.get(selected.get('lean')) + if expected and expected not in normalized: + raise ValueError(f'Guarded boundary changed its generated failure-capable signature: {selected["rust"]}') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('command', choices=['inputs', 'opaque', 'exclude']) + parser.add_argument('--root', type=Path, default=Path(__file__).resolve().parents[2]) + args = parser.parse_args() + if args.command == 'inputs': + print(json.dumps(input_identity(args.root), sort_keys=True)) + elif args.command == 'exclude': + print('\n'.join(EXCLUDED_PROVIDED_METHODS)) + else: + registry = json.loads((args.root / 'verification/aeneas/external.json').read_text()) + print('\n'.join(row['rust'] for row in registry if row.get('opaque'))) + + +if __name__ == '__main__': + main() diff --git a/verification/aeneas/build-aeneas.nix b/verification/aeneas/build-aeneas.nix index 94e454fbef..a019661511 100644 --- a/verification/aeneas/build-aeneas.nix +++ b/verification/aeneas/build-aeneas.nix @@ -23,11 +23,23 @@ let AENEAS_VERSION = builtins.getEnv "AENEAS_VERSION"; postInstall = ""; }); + charonBase = upstream.inputs.charon.packages.${system}; + charon = charonBase.charon-unwrapped.overrideAttrs (old: { + patches = (old.patches or []) ++ [ ./patches/admission-snapshot.patch ]; + }); + portableCharon = charonBase.charon-portable.overrideAttrs (_: { + unpackPhase = '' + mkdir bin + cp ${charon}/bin/charon ${charon}/bin/charon-driver bin/ + chmod -R u+w bin + ''; + }); in pkgs.runCommand "aeneas-nominal-bundle" { nativeBuildInputs = anneal.packages.${system}.aeneas-download.portabilityInputs; } '' mkdir -p $out cp ${aeneas}/bin/aeneas $out/aeneas + cp ${portableCharon}/bin/charon ${portableCharon}/bin/charon-driver $out/ ${pkgs.lib.optionalString pkgs.stdenv.isDarwin '' chmod +w $out/aeneas dylibbundler -od -b -x $out/aeneas -d $out/libs -p @executable_path/libs diff --git a/verification/aeneas/build-aeneas.sh b/verification/aeneas/build-aeneas.sh index 8a5ad39fcd..0751b80d52 100755 --- a/verification/aeneas/build-aeneas.sh +++ b/verification/aeneas/build-aeneas.sh @@ -10,7 +10,7 @@ set -euo pipefail cd "$(dirname "$0")/../.." [[ $# == 1 && -d "$1" ]] || { echo "Usage: $0 TOOLCHAIN_DIRECTORY" >&2; exit 1; } tools_dir=$(cd "$1" && pwd) -# Validate the producer archive before applying the consumer's CLI-only patch. +# Validate the producer archive before applying the consumer's source patches. values=$(python3 -B verification/aeneas/toolchain.py shell "$tools_dir" --upstream) eval "$values" command -v nix >/dev/null || { echo 'Building the patched Aeneas requires Nix.' >&2; exit 1; } @@ -45,4 +45,11 @@ if [[ -d "$artifact/libs" ]]; then # archive's libraries stay untouched in bundle/aeneas/bin/libs. cp -f "$artifact/libs/"* "$tools_dir/libs/" fi +# Keep archive executables intact. Admission uses a private driver copy with +# the pre-transformation snapshot patch, independently of Anneal's archive. +for name in charon charon-driver; do + [[ -L "$tools_dir/$name" ]] || { echo 'Expected fresh archive adapter' >&2; exit 1; } + rm "$tools_dir/$name" + cp "$artifact/$name" "$tools_dir/$name" +done python3 -B verification/aeneas/toolchain.py record "$tools_dir" diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py index 446e4785b0..d42318c462 100644 --- a/verification/aeneas/control_runner.py +++ b/verification/aeneas/control_runner.py @@ -26,7 +26,7 @@ import tempfile import time -FAMILIES = ('authoring', 'trait-rounding', 'coverage', 'abi', +FAMILIES = ('authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi', 'contracts', 'dependencies', 'admission', 'semantics') MODELS = ('golden-verification', 'verification') FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean', diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json new file mode 100644 index 0000000000..2ce379ce23 --- /dev/null +++ b/verification/aeneas/external.json @@ -0,0 +1,37 @@ +[ + {"rust": "core::array::{[T0;N0]}::as_slice", "signature": {"unsafe": false, "inputs": ["&[T0;N0]"], "output": "&[T0]", "types": 1, "consts": 1}, "lean": "Array.to_slice"}, + {"rust": "core::slice::index::{core::slice::index::SliceIndex}::index", "signature": {"unsafe": false, "inputs": ["usize", "&[T0]"], "output": "&T0", "types": 1, "consts": 0}, "lean": "core.slice.index.Usize.index", "before": {"rust": "core::slice::index::{core::slice::index::SliceIndex}::index", "signature": {"unsafe": false, "inputs": ["usize", "&[T0]"], "output": "&T0", "types": 1, "consts": 0}}}, + {"rust": "core::convert::{core::convert::Into}::into", "signature": {"unsafe": false, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.convert.IntoFrom.into"}, + {"rust": "core::num::{usize}::checked_mul", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option", "types": 0, "consts": 0}, "lean": "Usize.checked_mul"}, + {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero"], "output": "T0", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.get", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero"], "output": "T0", "types": 1, "consts": 0}}}, + {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option>", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.new", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option>", "types": 1, "consts": 0}}}, + {"rust": "core::num::{usize}::checked_sub", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option", "types": 0, "consts": 0}, "lean": "Usize.checked_sub"}, + {"rust": "core::fmt::{core::fmt::Arguments}::from_str", "signature": {"unsafe": false, "inputs": ["&str"], "output": "core::fmt::Arguments", "types": 0, "consts": 0}, "lean": "core.fmt.Arguments.from_str"}, + {"rust": "core::slice::{[T0]}::len", "signature": {"unsafe": false, "inputs": ["&[T0]"], "output": "usize", "types": 1, "consts": 0}, "lean": "Slice.len"}, + {"rust": "core::num::{usize}::is_power_of_two", "signature": {"unsafe": false, "inputs": ["usize"], "output": "bool", "types": 0, "consts": 0}, "lean": "core.num.Usize.is_power_of_two"}, + {"rust": "core::num::{usize}::leading_zeros", "signature": {"unsafe": false, "inputs": ["usize"], "output": "u32", "types": 0, "consts": 0}, "lean": "core.num.Usize.leading_zeros"}, + {"rust": "core::num::{usize}::checked_add", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option", "types": 0, "consts": 0}, "lean": "Usize.checked_add"}, + {"rust": "core::num::{usize}::wrapping_mul", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.wrapping_mul"}, + {"rust": "core::num::{usize}::wrapping_add", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.wrapping_add"}, + {"rust": "core::num::{usize}::wrapping_sub", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.wrapping_sub"}, + {"rust": "core::mem::align_of", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 1, "consts": 0}, "lean": "core.mem.align_of"}, + {"rust": "core::mem::size_of", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 1, "consts": 0}, "lean": "core.mem.size_of"}, + {"rust": "core::option::{core::option::Option}::is_some", "signature": {"unsafe": false, "inputs": ["&core::option::Option"], "output": "bool", "types": 1, "consts": 0}, "lean": "core.option.Option.is_some"}, + {"rust": "core::num::{usize}::unchecked_mul", "signature": {"unsafe": true, "inputs": ["usize", "usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.num.Usize.unchecked_mul"}, + {"rust": "core::num::{usize}::unchecked_add", "signature": {"unsafe": true, "inputs": ["usize", "usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.num.Usize.unchecked_add"}, + {"rust": "core::option::{core::option::Option}::is_none", "signature": {"unsafe": false, "inputs": ["&core::option::Option"], "output": "bool", "types": 1, "consts": 0}, "lean": "core.option.Option.is_none"}, + {"rust": "core::option::{core::option::Option}::unwrap", "signature": {"unsafe": false, "inputs": ["core::option::Option"], "output": "T0", "types": 1, "consts": 0}, "lean": "core.option.Option.unwrap"}, + {"rust": "zerocopy::util::transmute_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "util.transmute_unchecked", "opaque": true, "source_body_sha256": "58ee51c915af14bac8c12d66d5ac65feadf59742212c869c7f45f57f847d48b6"}, + {"rust": "zerocopy::util::copy_unchecked", "signature": {"unsafe": true, "inputs": ["&[u8]", "&mut [u8]"], "output": "tuple0", "types": 0, "consts": 0}, "lean": "util.copy_unchecked", "opaque": true, "source_body_sha256": "e3529644308d0a3ce1a407d163f98676faa36a286ba4a85221b894930d54fa20"}, + {"rust": "core::num::{u16}::from_be_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_be_bytes"}, + {"rust": "core::num::{u16}::from_le_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_le_bytes"}, + {"rust": "core::num::{u16}::to_be_bytes", "signature": {"unsafe": false, "inputs": ["u16"], "output": "[u8;2]", "types": 0, "consts": 0}, "lean": "core.num.U16.to_be_bytes"}, + {"rust": "core::num::{u16}::to_le_bytes", "signature": {"unsafe": false, "inputs": ["u16"], "output": "[u8;2]", "types": 0, "consts": 0}, "lean": "core.num.U16.to_le_bytes"}, + {"rust": "core::num::{u32}::from_be_bytes", "signature": {"unsafe": false, "inputs": ["[u8;4]"], "output": "u32", "types": 0, "consts": 0}, "lean": "core.num.U32.from_be_bytes"}, + {"rust": "core::num::{u32}::from_le_bytes", "signature": {"unsafe": false, "inputs": ["[u8;4]"], "output": "u32", "types": 0, "consts": 0}, "lean": "core.num.U32.from_le_bytes"}, + {"rust": "core::num::{u32}::to_be_bytes", "signature": {"unsafe": false, "inputs": ["u32"], "output": "[u8;4]", "types": 0, "consts": 0}, "lean": "core.num.U32.to_be_bytes"}, + {"rust": "core::num::{u32}::to_le_bytes", "signature": {"unsafe": false, "inputs": ["u32"], "output": "[u8;4]", "types": 0, "consts": 0}, "lean": "core.num.U32.to_le_bytes"}, + {"rust": "core::num::{usize}::MAX", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.MAX"}, + {"rust": "core::clone::impls::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.clone.CloneUsize"}, + {"rust": "core::num::niche_types::{core::clone::Clone}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"} +] diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index 252f1510d2..6914779356 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -52,6 +52,7 @@ def __init__(self): self.type_classes = None self.external_type_parameters = None self.source_snapshots = {} + self.source_body_digests = {} class GeneratedLines(list): @@ -468,6 +469,11 @@ def discover(root, tool): raise ValueError(f'{file}: {error}') from error encoded = source.encode('utf-8') annotations.source_snapshots[file] = encoded + if valid_file(file): + for owner in syntax[file].get('functions', []): + name = rust_identity(file, owner['path']) + annotations.source_body_digests.setdefault(name, []).append( + hashlib.sha256(encoded[owner['open']:owner['close']]).hexdigest()) if valid_file(file): for macro in syntax[file].get('macros', []): start = len(encoded[:macro['start']].decode('utf-8')) @@ -774,7 +780,13 @@ def save_bindings(root, annotations, work, development=False): 'category': category, 'parameters': declaration['parameters']}) if {row['rust'] for row in type_image if row['category'] == 'local-nominal'} != set(source_types): raise ValueError('Generated raw type image omits a source-bound nominal type') - manifest = {'version': 3, 'bindings': bindings, + import admission + admitted = None if development else admission.inspect(root, work, + [name for name, entry in bindings.items() if entry['kind'] == 'function'], + source_digest(root, annotations), annotations.source_body_digests) + if admitted is not None: + admission.check_translation(work, admitted) + manifest = {'version': 3, 'bindings': bindings, 'admission': admitted, 'type_image': type_image, 'mode': 'development' if development else 'verified-live', 'sources': source_digest(root, annotations), 'model': model_digest(work)} @@ -1007,6 +1019,8 @@ def identity(name): wrapped = implementation['skip_binder'] if set(wrapped) == {'Value'}: body = wrapped['Value'][1] + elif set(wrapped) == {'Untagged'}: + body = wrapped['Untagged'] elif set(wrapped) == {'Deduplicated'}: body = adts.get(wrapped['Deduplicated'], {}) else: @@ -1088,6 +1102,8 @@ def collect_type_values(value): and len(body[1]) == 1 and next(iter(body[1])) in type_tags): type_values.setdefault(body[0], []).append(body[1]) collect_type_values(body[1]) + elif tag == 'Untagged': + collect_type_values(body) elif tag in {'Array', 'Slice'} and isinstance(body, list) and body: collect_type_values(body[0]) elif tag == 'Adt' and isinstance(body, dict): @@ -1113,6 +1129,8 @@ def safe_field_type(ty, parameter_count, seen=frozenset()): if tag == 'Value': return (isinstance(body, list) and len(body) == 2 and isinstance(body[0], int) and safe_field_type(body[1], parameter_count, seen)) + if tag == 'Untagged': + return safe_field_type(body, parameter_count, seen) if tag == 'Deduplicated': if not isinstance(body, int) or body in seen: return False @@ -1315,6 +1333,10 @@ def main(): annotations = discover(args.root, args.tool) if args.command == 'bindings': check_bindings(args.root, annotations, args.work / 'zerocopy.llbc') + import admission + admission.inspect(args.root, args.work, + [name for name, entry in annotations.items() if entry.get('kind', 'function') == 'function'], + source_digest(args.root, annotations), annotations.source_body_digests) elif args.command == 'models': # The driver calls this only after bindings, on freshly generated live # output. Keep the verified mapping separate from mutable spec text. diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index 13df8e7041..8a7e3d6b0a 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -135,6 +135,24 @@ run_elab do | throwError "Model bindings must contain their source/extraction binding table" let .ok entries := entriesValue.getObj? | throwError "Model bindings must contain a binding table object" + if mode == "verified-live" then + let .ok admission := bindings.getObjVal? "admission" + | throwError "Missing mandatory execution admission evidence" + let .ok admissionVersion := admission.getObjValAs? Nat "version" + | throwError "Invalid execution admission evidence" + unless admissionVersion == 1 do + throwError "Unsupported execution admission evidence" + let .ok stages := admission.getObjVal? "stages" + | throwError "Missing execution admission stages" + let rootNames := entries.toArray.filterMap fun pair => + if pair.2.getObjValAs? String "kind" == .ok "function" then some pair.1 else none + for stage in #["before", "llbc"] do + let .ok evidence := stages.getObjVal? stage + | throwError "Missing {stage} execution admission stage" + let .ok roots := evidence.getObjValAs? (Array String) "roots" + | throwError "Invalid {stage} execution admission roots" + unless roots.size == rootNames.size && rootNames.all roots.contains do + throwError "Execution admission roots disagree with the function binding table" let some typesModule := env.getModuleIdx? `Zerocopy.Types | throwError "Raw extracted types must be imported" let some shapesModule := env.getModuleIdx? `ModelShapes @@ -276,6 +294,33 @@ run_elab do let extra := actualModels.filter (fun modelName => !expectedModels.contains modelName) unless missing.isEmpty && extra.isEmpty do throwError "Compiled inline specification models disagree with bindings: missing {missing}; unexpected {extra}" + -- The backend's Option.ofResult erases every failure into a normal None, + -- including undef. That is not a supported Rust recovery operation here. + -- Follow downstream compiled dependencies, including helpers and opaque + -- bodies, so hiding this adapter behind another local definition cannot + -- admit it. Stop at the pinned backend: its checked integer primitives use + -- this adapter internally to represent arithmetic overflow as Rust's None. + -- Their implementation is already part of the trusted translation boundary. + -- Identify that boundary by compiled module ownership, not a declaration's + -- namespace, so a downstream helper cannot impersonate a backend primitive. + -- This conservative check rejects even unreachable local dependencies; it + -- does not certify arbitrary external models as faithful Rust semantics. + let mut pendingModels := actualModels + let mut visitedModels : NameHashSet := {} + while !pendingModels.isEmpty do + let current := pendingModels.back! + pendingModels := pendingModels.pop + if visitedModels.contains current then continue + visitedModels := visitedModels.insert current + if current == `Aeneas.Std.Option.ofResult then + throwError "Extracted execution depends on unsupported failure erasure: {current}" + if let some owner := env.getModuleIdxFor? current then + let moduleName := env.allImportedModuleNames[owner.toNat]! + if moduleName.getRoot == `Aeneas && !auditModules.contains owner then continue + let some info := env.find? current + | throwError "Missing execution dependency {current}" + pendingModels := pendingModels ++ info.type.getUsedConstants ++ + ((info.value? (allowOpaque := true)).map (·.getUsedConstants)).getD #[] -- Sort only for reproducible diagnostics and dependency output. Coverage was -- established from complete sets above, independent of declaration order. required := required.qsort (fun a b => a.toString < b.toString) diff --git a/verification/aeneas/negative-control-extraction.sh b/verification/aeneas/negative-control-extraction.sh index dc1543aa26..a8d9f8a4d3 100644 --- a/verification/aeneas/negative-control-extraction.sh +++ b/verification/aeneas/negative-control-extraction.sh @@ -20,6 +20,9 @@ run() { python3 -B verification/aeneas/control_runner.py command \ "$AENEAS_CONTROL_LOG_DIR/commands" -- "$@" } +run python3 -B verification/aeneas/tests/provided_method_controls.py \ + "$tools_dir/charon" "$work" "$repo" "$tools_dir/rust/lib" +run bash verification/aeneas/tests/annotation-origins.sh "$tools_dir/charon" "$tools_dir/rust/lib" # Validate capability observations before interpreting absence as inapplicability. capabilities=$(python3 - "$project/bindings.json" <<'PY' import json, sys diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh index dff1a3ebdd..56f2eca8de 100644 --- a/verification/aeneas/negative-control-family.sh +++ b/verification/aeneas/negative-control-family.sh @@ -226,7 +226,34 @@ restore_build() { } if [[ $AENEAS_CONTROL_FAMILY == unsafe ]]; then -: # This family has no controls before its introducing feature. +# An opaque helper must not conceal an adapter which discards forbidden +# failures. This mutation leaves NonZero::get's returned value unchanged, so +# ordinary functional proofs alone would not detect the unsupported dependency. +# Its backend-like namespace must not hide its actual downstream module owner. +python3 - <<'PYCONTROL' +from pathlib import Path +p = Path("Zerocopy/FunsExternal.lean") +s = p.read_text() +start = "@[simp] def core.num.nonzero.NonZero.get" +body = "(x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val" +if s.count(start) != 1 or s.count(body) != 1: + raise SystemExit("Failure erasure control no longer matches") +helper = ("opaque Aeneas.Std.hiddenFailureErasure : Option Unit :=\n" + " Aeneas.Std.Option.ofResult (Result.fail .undef : Result Unit)\n\n") +s = s.replace(start, helper + start) +s = s.replace(body, "(x : core.num.nonzero.NonZero T Inner) : Result T :=\n" + " match Aeneas.Std.hiddenFailureErasure with\n" + " | none => .ok x.val\n" + " | some _ => .ok x.val") +p.write_text(s) +PYCONTROL +check_model_mutant "failure erasure hidden behind an opaque helper" Zerocopy.FunsExternal +expect_failure "failure erasure hidden behind an opaque helper" unsafe-erasure-audit.log audit +if ! grep -Fq 'unsupported failure erasure' "$backup/unsafe-erasure-audit.log"; then + cat "$backup/unsafe-erasure-audit.log" >&2; exit 1 +fi +restore_build + fi # unsafe if [[ $AENEAS_CONTROL_FAMILY == coverage ]]; then @@ -408,6 +435,10 @@ if len(keys) != 1: raise SystemExit("Binding-image control requires a unique min mapping") if mutation == "missing-map": del models[keys[0]] + # Keep the admission roster internally consistent so this control reaches + # the independent compiled-root coverage check it is intended to challenge. + for stage in manifest.get("admission", {}).get("stages", {}).values(): + stage["roots"].remove(keys[0]) manifest_path.write_text(json.dumps(manifest, indent=2) + '\n') elif mutation == "duplicate-map": if [entry["raw"] for entry in models.values()].count("Zerocopy.util.max") != 1: diff --git a/verification/aeneas/patches/admission-snapshot.patch b/verification/aeneas/patches/admission-snapshot.patch new file mode 100644 index 0000000000..2559188599 --- /dev/null +++ b/verification/aeneas/patches/admission-snapshot.patch @@ -0,0 +1,500 @@ +--- a/src/bin/charon-driver/main.rs ++++ b/src/bin/charon-driver/main.rs +@@ -91,0 +92,15 @@ ++ // Preserve executable effects before any Charon simplification. The consumer ++ // requires this snapshot, so a stock driver cannot silently skip admission. ++ // This is evidence for a downstream checker, not a rustc correctness proof. ++ if let Some(path) = std::env::var_os("CHARON_ADMISSION_SNAPSHOT") { ++ let snapshot = export::CrateData { ++ charon_version: export::CharonVersion(charon_lib::VERSION.to_owned()), ++ translated: ctx.translated.clone(), ++ has_errors: ctx.errors.borrow().error_count != 0, ++ }; ++ snapshot.serialize_to_file( ++ std::path::Path::new(&path), ++ charon_lib::options::SerializationFormat::Json, ++ ).map_err(|()| CharonFailure::Serialize)?; ++ } ++ +--- a/src/bin/charon-driver/translate/get_mir.rs ++++ b/src/bin/charon-driver/translate/get_mir.rs +@@ -87 +87,9 @@ +- // We fall back to optimized MIR if the requested body was stolen. ++ // Admission must inspect the requested pre-optimization body. ++ // A stolen local body cannot silently become optimized MIR. ++ // None leaves a missing body which the consumer rejects. ++ if std::env::var_os("CHARON_ADMISSION_SNAPSHOT").is_some() ++ && !matches!(level, MirLevel::Optimized) ++ { ++ return None; ++ } ++ // Other consumers retain the upstream fallback behavior. +--- a/src/bin/charon-driver/translate/translate_crate.rs ++++ b/src/bin/charon-driver/translate/translate_crate.rs +@@ -29 +29 @@ +-use charon_lib::options::{CliOpts, ConstHandling, StartFrom, TranslateOptions}; ++use charon_lib::options::{CliOpts, ConstHandling, SourceOwnerSpan, StartFrom, TranslateOptions}; +@@ -376,0 +377,114 @@ ++ }) ++ } ++ ++ fn matches_source_owner(&mut self, owner: &SourceOwnerSpan, span: rustc_span::Span) -> bool { ++ if span.is_dummy() { ++ return false; ++ } ++ let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo()); ++ matches!(self.translate_filename(source_file.name.clone()), FileName::Local(path) if path == owner.file) ++ && source_file.original_relative_byte_pos(span.lo()).0 == owner.beg ++ && source_file.original_relative_byte_pos(span.hi()).0 == owner.end ++ } ++ ++ // This census is deliberately collected before root selection. Owner attribute maps ++ // include unsupported fields, variants, generics and statement docs omitted by the ++ // item iterator. Classify the attributed node, never just its enclosing owner. ++ fn annotation_origins(&mut self) -> Vec<(rustc_span::def_id::LocalDefId, serde_json::Value)> { ++ use rustc_ast::token::DocFragmentKind; ++ use rustc_hir::{Attribute, Node, attrs::AttributeKind, def::DefKind}; ++ let tcx = self.tcx; ++ let mut nodes = Vec::new(); ++ for owner in tcx.hir_crate_items(()).owners() { ++ for (local_id, attrs) in tcx.hir_attr_map(owner).map.iter() { ++ let hir_id = rustc_hir::HirId { ++ owner, ++ local_id: *local_id, ++ }; ++ // rustc lowering aliases a tuple/unit struct's complete attribute ++ // slice onto its synthetic constructor. There is no separately ++ // authored constructor declaration. Canonicalize only this exact ++ // compiler alias, verified against the nominal item's HIR data, ++ // owner, constructor DefId parent, and identical attribute slice. ++ // Variant constructors and all fields remain unsupported nodes. ++ if let Node::Ctor(data) = tcx.hir_node(hir_id) ++ && let Node::Item(parent) = tcx.parent_hir_node(hir_id) ++ && let rustc_hir::ItemKind::Struct(_, _, nominal_data) = &parent.kind ++ && let Some((_, ctor_hir_id, ctor_def_id)) = data.ctor() ++ && ctor_hir_id == hir_id ++ && std::ptr::eq(data, nominal_data) ++ && parent.owner_id == owner ++ && tcx.local_def_id_to_hir_id(owner.def_id) == parent.hir_id() ++ && tcx.parent(ctor_def_id.to_def_id()) == parent.owner_id.def_id.to_def_id() ++ && std::ptr::eq(*attrs, tcx.hir_attrs(parent.hir_id())) ++ { ++ continue; ++ } ++ let mut docs = Vec::new(); ++ for attr in *attrs { ++ if let Attribute::Parsed(AttributeKind::DocComment { ++ style, ++ kind, ++ span, ++ comment, ++ }) = attr ++ { ++ // A forwarded literal's value span remains authored even when ++ // the complete attribute span is synthesized by expansion. ++ let origin = match kind { ++ DocFragmentKind::Raw(value_span) => *value_span, ++ DocFragmentKind::Sugared(_) => *span, ++ }; ++ let mut doc = self.annotation_span(origin); ++ doc["text"] = serde_json::json!(comment.as_str()); ++ doc["outer"] = serde_json::json!(*style == rustc_ast::AttrStyle::Outer); ++ docs.push(doc); ++ } ++ } ++ if docs.is_empty() { ++ continue; ++ } ++ let ldid = owner.def_id; ++ let is_owner = tcx.local_def_id_to_hir_id(ldid) == hir_id; ++ let kind = if is_owner { ++ match tcx.def_kind(ldid) { ++ DefKind::Fn | DefKind::AssocFn => "function", ++ DefKind::Struct | DefKind::Enum | DefKind::Union | DefKind::TyAlias => { ++ "type" ++ } ++ DefKind::Trait => "trait", ++ DefKind::Impl { of_trait: true } => "trait-impl", ++ _ => "unsupported", ++ } ++ } else { ++ "unsupported" ++ }; ++ let span = match tcx.hir_node(hir_id) { ++ Node::Item(item) => item.span, ++ Node::TraitItem(item) => item.span, ++ Node::ImplItem(item) => item.span, ++ _ => tcx.hir_span(hir_id), ++ }; ++ nodes.push((ldid, serde_json::json!({ ++ "owner": tcx.def_path_str(ldid.to_def_id()), ++ "node_kind": kind, ++ "positive": kind == "trait-impl" && tcx.impl_polarity(ldid) == ty::ImplPolarity::Positive, ++ "span": self.annotation_span(span), ++ "docs": docs, ++ "trait_impl_id": null, ++ }))); ++ } ++ } ++ nodes ++ } ++ ++ fn annotation_span(&mut self, span: rustc_span::Span) -> serde_json::Value { ++ let source = self.tcx.sess.source_map().lookup_source_file(span.lo()); ++ let file = match self.translate_filename(source.name.clone()) { ++ FileName::Local(path) => path.to_string_lossy().into_owned(), ++ _ => source.name.prefer_local_unconditionally().to_string(), ++ }; ++ serde_json::json!({ ++ "file": file, ++ "begin": source.original_relative_byte_pos(span.lo()).0, ++ "end": source.original_relative_byte_pos(span.hi()).0, +@@ -1036,0 +1151,24 @@ ++ // A provided method omitted from its trait dictionary cannot be called. Check the ++ // compiler-resolved declaration, including inherited and overridden implementations, ++ // before translating its signature. Impl discovery uses the no-enqueue path. ++ if enqueue && let hax::FullDefKind::AssocFn(f) = self.poly_hax_def(&item.def_id)?.kind() { ++ let declaration_id = f.associated_item().implemented_trait_item_id(); ++ let declaration = self.poly_hax_def(declaration_id)?; ++ if let hax::FullDefKind::AssocFn(declaration) = declaration.kind() ++ && declaration.associated_item().has_value ++ && matches!( ++ &declaration.associated_item().container, ++ hax::AssocItemContainer::TraitContainer { .. } ++ ) ++ { ++ let source = TransItemSource::polymorphic(declaration_id, TransItemSourceKind::Fun); ++ let name = self.translate_name(&source)?; ++ if self.opacity_for_name(&name).is_invisible() { ++ charon_lib::errors::raise_error!( ++ self, ++ span, ++ "referenced excluded provided trait method" ++ ); ++ } ++ } ++ } +@@ -1189,0 +1328,40 @@ ++ if ctx.options.monomorphize_with_hax ++ && (std::env::var_os("CHARON_ANNOTATION_ORIGINS").is_some() ++ || ctx ++ .options ++ .start_from ++ .iter() ++ .any(|root| matches!(root, StartFrom::DocOrigin(_)))) ++ { ++ register_error!( ++ ctx, ++ Span::dummy(), ++ "annotation-origin evidence requires polymorphic translation" ++ ); ++ return Err(Error::dummy()); ++ } ++ let mut annotation_origins = ctx.annotation_origins(); ++ // Bind the census to the compiler's complete local source inputs, including ++ // macro definitions with no docs. This reads rustc's captured normalized text, ++ // not files that could have changed after compilation. ++ let source_files = tcx.sess.source_map().files().iter().cloned().collect_vec(); ++ let annotation_sources = source_files ++ .into_iter() ++ .filter_map(|source| { ++ let FileName::Local(file) = ctx.translate_filename(source.name.clone()) else { ++ return None; ++ }; ++ if file.as_os_str().is_empty() ++ || file ++ .components() ++ .any(|c| !matches!(c, std::path::Component::Normal(_))) ++ { ++ return None; ++ } ++ source ++ .src ++ .as_ref() ++ .map(|text| serde_json::json!({"file":file,"text":text.as_str()})) ++ }) ++ .collect_vec(); ++ +@@ -1199,0 +1378,77 @@ ++ } ++ StartFrom::SourceSpan(owner) => { ++ // Resolve against compiler owners, never against names, generics, or doc text. ++ let mut matches = Vec::new(); ++ for ldid in tcx.hir_crate_items(()).definitions() { ++ // `def_span` is only an impl header; the HIR item span covers ++ // the exact authored owner, including its closing brace. ++ let rustc_hir::Node::Item(item) = ++ tcx.hir_node(tcx.local_def_id_to_hir_id(ldid)) ++ else { ++ continue; ++ }; ++ let span = item.span; ++ if span.is_dummy() { ++ continue; ++ } ++ if ctx.matches_source_owner(&owner, span) ++ || (span.from_expansion() ++ && ctx.matches_source_owner(&owner, span.source_callsite())) ++ { ++ matches.push((ldid, span)); ++ } ++ } ++ if matches.len() != 1 { ++ register_error!( ++ ctx, ++ Span::dummy(), ++ "source-owner root {owner:?} matched {} local owners; expected exactly one", ++ matches.len() ++ ); ++ continue; ++ } ++ let (ldid, span) = matches[0]; ++ if span.from_expansion() ++ || !matches!( ++ tcx.def_kind(ldid), ++ rustc_hir::def::DefKind::Impl { of_trait: true } ++ ) ++ || tcx.impl_polarity(ldid) != ty::ImplPolarity::Positive ++ { ++ let error_span = ctx.translate_span(&span); ++ register_error!( ++ ctx, ++ error_span, ++ "source-owner root requires a non-expanded positive trait impl" ++ ); ++ continue; ++ } ++ let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state); ++ ctx.enqueue_module_item(&def_id, true); ++ } ++ StartFrom::DocOrigin(origin) => { ++ let matches = annotation_origins ++ .iter() ++ .filter(|(_, node)| { ++ node["node_kind"] == "trait-impl" ++ && node["positive"] == true ++ && node["docs"].as_array().unwrap().iter().any(|doc| { ++ doc["outer"] == true ++ && doc["file"].as_str() == origin.file.to_str() ++ && doc["begin"].as_u64() == Some(u64::from(origin.beg)) ++ && doc["end"].as_u64() == Some(u64::from(origin.end)) ++ }) ++ }) ++ .map(|(ldid, _)| *ldid) ++ .collect_vec(); ++ if matches.len() != 1 { ++ register_error!( ++ ctx, ++ Span::dummy(), ++ "doc-origin root {origin:?} matched {} positive local trait impls; expected exactly one", ++ matches.len() ++ ); ++ continue; ++ } ++ let def_id: hax::DefId = matches[0].to_def_id().sinto(&ctx.hax_state); ++ ctx.enqueue_module_item(&def_id, true); +@@ -1262,0 +1518,37 @@ ++ if let Some(path) = std::env::var_os("CHARON_ANNOTATION_ORIGINS") { ++ for (ldid, node) in &mut annotation_origins { ++ if node["node_kind"] == "trait-impl" { ++ let def_id: hax::DefId = ldid.to_def_id().sinto(&ctx.hax_state); ++ let source = TransItemSource::polymorphic( ++ &def_id, ++ TransItemSourceKind::TraitImpl(TransImplSource::Normal), ++ ); ++ if let Some(ItemId::TraitImpl(id)) = ctx.id_map.get(&source) { ++ node["trait_impl_id"] = serde_json::json!(id.index()); ++ // The consumer compares this exact original dictionary with ++ // the admission snapshot before using the id in final LLBC. ++ node["trait_impl"] = ++ serde_state_perfect_derive::SerializeState::serialize_state( ++ &ctx.translated.trait_impls.get(*id), ++ &(), ++ serde_json::value::Serializer, ++ ) ++ .expect("native trait dictionary serializes to JSON"); ++ } ++ } ++ } ++ let output = serde_json::json!({"version": 1, "sources": annotation_sources, ++ "nodes": annotation_origins.into_iter().map(|(_, node)| node).collect_vec()}); ++ if let Err(error) = std::fs::File::create(path) ++ .map_err(|e| e.to_string()) ++ .and_then(|file| serde_json::to_writer(file, &output).map_err(|e| e.to_string())) ++ { ++ register_error!( ++ ctx, ++ Span::dummy(), ++ "cannot write annotation origins: {error}" ++ ); ++ return Err(Error::dummy()); ++ } ++ } ++ +--- a/src/bin/charon-driver/translate/translate_items.rs ++++ b/src/bin/charon-driver/translate/translate_items.rs +@@ -902,0 +903,6 @@ ++ // Excluded provided methods have neither a dictionary field nor a default ++ // body. Do not translate their signatures: even an unused signature can ++ // import unrelated traits and types. The method id remains allocated. ++ if hax_item.has_value && method_opacity.is_invisible() { ++ continue; ++ } +@@ -1209,0 +1216,14 @@ ++ // Match the trait declaration's exclusion even when this impl overrides ++ // the default. Discovery is not a call and must not import its signature. ++ let declaration_id = impl_item.decl_def_id(); ++ let declaration = self.poly_hax_def(declaration_id)?; ++ if let hax::FullDefKind::AssocFn(declaration) = declaration.kind() ++ && declaration.associated_item().has_value ++ { ++ let source = ++ TransItemSource::polymorphic(declaration_id, TransItemSourceKind::Fun); ++ let name = self.translate_name(&source)?; ++ if self.opacity_for_name(&name).is_invisible() { ++ continue; ++ } ++ } +--- a/src/options.rs ++++ b/src/options.rs +@@ -91,0 +92,5 @@ ++ /// An exact local positive trait impl can instead be selected with ++ /// `@span:FILE:BEGIN_BYTE:END_BYTE`, using its full authored HIR item span. ++ /// Macro impls can use `@doc-origin:FILE:BEGIN_BYTE:END_BYTE` to select the ++ /// unique positive impl carrying that outer authored doc fragment. ++ /// FILE is normalized crate-relative; offsets are UTF-8 bytes, end exclusive. +@@ -677,0 +683,37 @@ ++/// Exact source owner selector; deliberately independent of Rust name/type spelling. ++#[derive(Debug, Clone, PartialEq, Eq)] ++pub struct SourceOwnerSpan { ++ pub file: PathBuf, ++ pub beg: u32, ++ pub end: u32, ++} ++ ++impl SourceOwnerSpan { ++ fn parse(value: &str) -> Result { ++ let parts = value.rsplitn(3, ':').collect_vec(); ++ if parts.len() != 3 { ++ return Err("expected FILE:BEGIN_BYTE:END_BYTE".into()); ++ } ++ let number = |s: &str| { ++ s.parse::() ++ .map_err(|_| "invalid coordinate".to_owned()) ++ }; ++ let file = PathBuf::from(parts[2]); ++ // No path aliases: admission can compare the requested owner list literally. ++ if file.as_os_str().is_empty() ++ || file.components().collect::().as_os_str() != file.as_os_str() ++ || file ++ .components() ++ .any(|c| !matches!(c, std::path::Component::Normal(_))) ++ { ++ return Err("FILE must be a normalized crate-relative path".into()); ++ } ++ let beg = number(parts[1])?; ++ let end = number(parts[0])?; ++ if beg >= end { ++ return Err("expected a nonempty, ordered byte span".into()); ++ } ++ Ok(Self { file, beg, end }) ++ } ++} ++ +@@ -685,0 +728,4 @@ ++ /// Exact local positive trait-impl owner. ++ SourceSpan(SourceOwnerSpan), ++ /// Positive trait impl uniquely carrying a physical authored doc fragment. ++ DocOrigin(SourceOwnerSpan), +@@ -787 +833 @@ +- let mut parse_pattern = |s: &str| -> Result<_, Error> { ++ fn parse_pattern(error_ctx: &mut ErrorCtx, s: &str) -> Result { +@@ -792 +838 @@ +- }; ++ } +@@ -799,9 +845,55 @@ +- let mut start_from = options +- .start_from +- .iter() +- .filter_map(|path| parse_pattern(path).ok()) +- .map(|p| StartFrom::Pattern { +- pattern: p, +- strict: true, +- }) +- .collect_vec(); ++ let mut start_from = Vec::new(); ++ for value in &options.start_from { ++ if let Some(value) = value.strip_prefix("@span:") { ++ match SourceOwnerSpan::parse(value) { ++ Ok(span) => { ++ if start_from.iter().any( ++ |root| matches!(root, StartFrom::SourceSpan(other) if other == &span), ++ ) { ++ register_error!( ++ error_ctx, ++ no_crate, ++ "duplicate source-owner root `{value}`" ++ ); ++ } else { ++ start_from.push(StartFrom::SourceSpan(span)); ++ } ++ } ++ Err(message) => { ++ register_error!( ++ error_ctx, ++ no_crate, ++ "invalid source-owner root `{value}`: {message}" ++ ); ++ } ++ } ++ } else if let Some(value) = value.strip_prefix("@doc-origin:") { ++ match SourceOwnerSpan::parse(value) { ++ Ok(origin) => { ++ if start_from.iter().any( ++ |root| matches!(root, StartFrom::DocOrigin(other) if other == &origin), ++ ) { ++ register_error!( ++ error_ctx, ++ no_crate, ++ "duplicate doc-origin root `{value}`" ++ ); ++ } else { ++ start_from.push(StartFrom::DocOrigin(origin)); ++ } ++ } ++ Err(message) => { ++ register_error!( ++ error_ctx, ++ no_crate, ++ "invalid doc-origin root `{value}`: {message}" ++ ); ++ } ++ } ++ } else if let Ok(pattern) = parse_pattern(error_ctx, value) { ++ start_from.push(StartFrom::Pattern { ++ pattern, ++ strict: true, ++ }); ++ } ++ } +@@ -812 +904 @@ +- .filter_map(|path| parse_pattern(path).ok()) ++ .filter_map(|path| parse_pattern(error_ctx, path).ok()) +@@ -824 +916,2 @@ +- if start_from.is_empty() { ++ // An invalid explicit root must never fall back to extracting the whole crate. ++ if start_from.is_empty() && options.start_from.is_empty() { +@@ -826 +919 @@ +- pattern: parse_pattern("crate").unwrap(), ++ pattern: parse_pattern(error_ctx, "crate").unwrap(), +@@ -843 +936 @@ +- .filter_map(|s| parse_pattern(s).ok()) ++ .filter_map(|s| parse_pattern(error_ctx, s).ok()) +@@ -890 +983,3 @@ +- .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity))) ++ .filter_map(|(s, opacity)| { ++ parse_pattern(error_ctx, &s).ok().map(|pat| (pat, opacity)) ++ }) +@@ -898 +993 @@ +- .filter_map(|s| parse_pattern(s).ok()) ++ .filter_map(|s| parse_pattern(error_ctx, s).ok()) diff --git a/verification/aeneas/run.sh b/verification/aeneas/run.sh index 8180f33bdc..11020b14a0 100755 --- a/verification/aeneas/run.sh +++ b/verification/aeneas/run.sh @@ -36,7 +36,7 @@ initialize_workspace() { "${workspace_cmd[@]}" initialize "$1" --root "$repo" --backend "$backend" } check_proofs() { - "${workspace_cmd[@]}" check "$1" --root "$repo" + "${workspace_cmd[@]}" verify "$1" --root "$repo" } work="$repo/target/aeneas/verification" golden_work="$repo/target/aeneas/golden-verification" @@ -54,6 +54,19 @@ scan=scan if "$update_goldens"; then scan=scan-update; fi "${inline_cmd[@]}" "$scan" "${inline_args[@]}" --work "$work" roots=$(cat "$work/roots.txt") +# Admission requires controlled compiler inputs and both inspection stages. +# Registry-derived opaque selections cannot hide arbitrary local functions. +python3 -B verification/aeneas/admission.py inputs > "$work/extraction-inputs.json" +opaque_args=() +while IFS= read -r name; do + [[ -z "$name" ]] || opaque_args+=(--opaque "$name") +done < <(python3 -B verification/aeneas/admission.py opaque) +excluded_args=() +while IFS= read -r name; do + [[ -z "$name" ]] || excluded_args+=(--exclude "$name") +done < <(python3 -B verification/aeneas/admission.py exclude) +export CHARON_ADMISSION_SNAPSHOT="$work/zerocopy.before.ullbc" +export CHARON_ANNOTATION_ORIGINS="$work/annotation-origins.json" # This compiles the actual zerocopy library with its normal build script and # default features. Start from these private helpers and their dependencies; @@ -63,17 +76,28 @@ roots=$(cat "$work/roots.txt") CARGO_TARGET_DIR="$repo/target/aeneas/rust" \ "$tools_dir/charon" cargo --preset=aeneas --sysroot default \ --start-from "$roots" \ + --mir promoted --no-dedup-serialized-ast \ + "${opaque_args[@]}" \ + "${excluded_args[@]}" \ --dest-file "$work/zerocopy.llbc" --abort-on-error --error-on-warnings \ -- --lib --locked --offline ) # Charon produces LLBC; the inline tool binds Rust owners to that inspected # extraction. Aeneas then produces the function bodies used by the live proofs. +# Admission inspects the preserved pre-transformation snapshot and final LLBC. +# Their remaining correspondence premises are recorded in LOWERING_AUDIT.md. +# FIXME: Typed copies erase storage events (upstream issue #1405): +# https://github.com/AeneasVerif/aeneas/issues/1405. Neither strict extraction +# errors nor the downstream forbidden tag can detect an already erased effect. +# Promoted MIR precedes drop elaboration: residual Drop terminators reject the +# body rather than relying on destructor desugaring or Aeneas's drop erasure. python3 verification/aeneas/prepare.py llbc "$work/zerocopy.llbc" "${inline_cmd[@]}" bindings "${inline_args[@]}" --work "$work" "$tools_dir/aeneas" -backend lean -namespace Zerocopy -dest "$work/Zerocopy" \ -split-files -abort-on-error -warnings-as-errors -no-progress-bar \ -use-tuple-structs false \ "$work/zerocopy.llbc" +unset CHARON_ADMISSION_SNAPSHOT CHARON_ANNOTATION_ORIGINS python3 verification/aeneas/prepare.py prepare "$work" "${inline_cmd[@]}" models "${inline_args[@]}" --work "$work" "${inline_cmd[@]}" assemble "${inline_args[@]}" --work "$work" diff --git a/verification/aeneas/tests/admission/README.md b/verification/aeneas/tests/admission/README.md new file mode 100644 index 0000000000..fd9a6056d2 --- /dev/null +++ b/verification/aeneas/tests/admission/README.md @@ -0,0 +1,14 @@ +# Admission fixture + +`boolean.before.ullbc` contains the two function declarations and value carriers +needed by `checked_bool` from the pinned Charon 0.1.276 promoted-MIR extraction. +Unrelated declarations and crate bookkeeping are omitted; executable bodies, +signatures, attributes, options, and target information remain from the actual +extraction. JSON whitespace is compressed to avoid a large generated diff. + +Regenerate with `run.sh --extract-only`, then select `checked_bool`, +`transmute_unchecked`, the unit carrier, and `Option` from +`target/aeneas/verification/zerocopy.before.ullbc`. Keep the options profile intact. +The mutation tests never execute invalid Rust; they challenge admission of the +compiler's intermediate representation. Lean and native Rust tests check the +accepted helper models and safe callers separately. diff --git a/verification/aeneas/tests/admission/boolean.before.ullbc b/verification/aeneas/tests/admission/boolean.before.ullbc new file mode 100644 index 0000000000..f0256d1f10 --- /dev/null +++ b/verification/aeneas/tests/admission/boolean.before.ullbc @@ -0,0 +1 @@ +{"charon_version":"0.1.276","has_errors":false,"translated":{"crate_name":"zerocopy","options":{"ullbc":false,"precise_drops":false,"mir":"Promoted","rustc_args":[],"targets":[],"sysroot":"default","monomorphize":false,"monomorphize_mut":null,"start_from":["zerocopy::byteorder::verification::read_u16_le","zerocopy::byteorder::verification::write_u16_le","zerocopy::byteorder::verification::set_u16_le","zerocopy::byteorder::verification::read_u16_be","zerocopy::byteorder::verification::write_u16_be","zerocopy::byteorder::verification::set_u16_be","zerocopy::byteorder::verification::read_u32_le","zerocopy::byteorder::verification::write_u32_le","zerocopy::byteorder::verification::set_u32_le","zerocopy::byteorder::verification::read_u32_be","zerocopy::byteorder::verification::write_u32_be","zerocopy::byteorder::verification::set_u32_be","zerocopy::layout::cast_from::CastPlan::size_sequences_match","zerocopy::layout::cast_from::CastPlan::try_compute","zerocopy::layout::cast_from::CastPlan::cast_metadata","zerocopy::layout::cast_from::checks::assert_cast_preserves_size","zerocopy::layout::composition_checks::check_extend","zerocopy::layout::composition_checks::check_pad","zerocopy::layout::composition_checks::check_constructor","zerocopy::layout::RoundingAlignAndPhase::new","zerocopy::layout::RoundingAlignAndPhase::components","zerocopy::layout::RoundingAlignAndPhase::align","zerocopy::layout::TrailingSliceLayout::size_offset","zerocopy::layout::TrailingSliceLayout::max_trailing_bytes","zerocopy::layout::TrailingSliceLayout::padding_for_elems","zerocopy::layout::TrailingSliceLayout::size_for_elems","zerocopy::layout::TrailingSliceLayout::has_same_size_sequence","zerocopy::layout::TrailingSliceLayout::advance","zerocopy::layout::SizeInfo::try_to_nonzero_elem_size","zerocopy::layout::max_elems_for_bytes","zerocopy::layout::DstLayout::assume_shallow_unpadded","zerocopy::layout::DstLayout::new_zst","zerocopy::layout::DstLayout::for_type","zerocopy::layout::DstLayout::for_unpadded_type","zerocopy::layout::DstLayout::for_slice","zerocopy::layout::DstLayout::for_repr_c_struct","zerocopy::layout::DstLayout::extend","zerocopy::layout::DstLayout::pad_to_align","zerocopy::layout::DstLayout::requires_static_padding","zerocopy::layout::DstLayout::requires_dynamic_padding","zerocopy::layout::DstLayout::metadata_for_exact_size","zerocopy::layout::DstLayout::validate_cast_and_convert_metadata","zerocopy::layout::add_scaled_metadata","zerocopy::layout::RoundingAlignAndPhase","zerocopy::layout::nested_reference::round_up","zerocopy::layout::nested_reference::size_for_metadata","zerocopy::layout::nested_reference::assert_matches_dst_layout","zerocopy::layout::primitive_checks::check_primitive_layouts","zerocopy::layout::primitive_checks::check_empty_layout","zerocopy::layout::tail_checks::trailing_arithmetic_check","zerocopy::layout::tail_checks::layout_observations_check","zerocopy::layout::tail_transform_checks::tail_transformations_check","zerocopy::layout::tail_transform_checks::tail_size_sequence_check","zerocopy::layout::tail_transform_checks::tail_dynamic_padding_check","zerocopy::pointer_metadata_unit_from_elem_count","zerocopy::pointer_metadata_unit_to_elem_count","zerocopy::pointer_metadata_unit_size_for_metadata","zerocopy::pointer_metadata_usize_from_elem_count","zerocopy::pointer_metadata_usize_to_elem_count","zerocopy::pointer_metadata_usize_size_for_metadata","zerocopy::pointer::cast::cast_unsized_layouts_match","zerocopy::pointer::cast::checks::assert_cast_unsized","zerocopy::split_at::split_right_len","zerocopy::split_at::split_zero_padding","zerocopy::split_at::numerical_checks::check_split_geometry","zerocopy::util::allocation::prepare","zerocopy::util::allocation::assert_preparation","zerocopy::util::allocation::assert_allocation_size","zerocopy::util::checks::check_arithmetic","zerocopy::util::padding_needed_for","zerocopy::util::round_down_to_next_multiple_of_alignment","zerocopy::util::max","zerocopy::util::min","zerocopy::util::safety_checks::checked_bool","zerocopy::util::safety_checks::checked_copy"],"start_from_if_exists":[],"start_from_attribute":[],"start_from_pub":false,"include":[],"opaque":["zerocopy::util::transmute_unchecked","zerocopy::util::copy_unchecked"],"exclude":[],"extract_opaque_bodies":false,"translate_all_methods":false,"eager_vtables":false,"duplicate_defaulted_methods":false,"lift_associated_types":["*"],"hide_marker_traits":true,"hide_allocator":true,"no_doc_comments":false,"remove_unused_clauses":false,"remove_unused_self_clauses":true,"remove_adt_clauses":true,"desugar_drops":false,"resugar_drops":false,"detect_drop_flags":false,"ops_to_function_calls":true,"index_to_function_calls":true,"treat_box_as_builtin":true,"no_gen_tuple_structs":true,"raw_consts":false,"consts":null,"unsized_strings":false,"reconstruct_fallible_operations":true,"reconstruct_asserts":true,"reconstruct_matches":true,"deallocate_all_locals":true,"unbind_item_vars":true,"print_original_ullbc":false,"print_ullbc":false,"print_built_llbc":false,"print_llbc":false,"print_layouts":false,"dest_dir":null,"dest_file":"/Users/codex/Codex/Migrated/zerocopy/aeneas-ci/worktrees/main/.aeneas-work/aeneas-shared-review-20261008/target/aeneas/verification/zerocopy.llbc","no_dedup_serialized_ast":true,"format":null,"no_serialize":false,"skip_borrowck":false,"erase_body_lifetimes":false,"no_typecheck":false,"no_normalize":false,"no_reorder_decls":false,"no_compute_layout_guarantees":false,"abort_on_error":true,"error_on_warnings":true,"preset":"Aeneas"},"target_information":[{"key":"aarch64-apple-darwin","value":{"target_pointer_size":8,"is_little_endian":true,"c_enum_smallest_repr_ty":"I32","primitive_alignments":[{"key":"Bool","value":1},{"key":{"Integer":{"Signed":"I8"}},"value":1},{"key":{"Integer":{"Signed":"I16"}},"value":2},{"key":{"Integer":{"Signed":"I32"}},"value":4},{"key":{"Integer":{"Signed":"I64"}},"value":8},{"key":{"Integer":{"Signed":"I128"}},"value":16},{"key":{"Integer":{"Signed":"Isize"}},"value":8},{"key":{"Integer":{"Unsigned":"U8"}},"value":1},{"key":{"Integer":{"Unsigned":"U16"}},"value":2},{"key":{"Integer":{"Unsigned":"U32"}},"value":4},{"key":{"Integer":{"Unsigned":"U64"}},"value":8},{"key":{"Integer":{"Unsigned":"U128"}},"value":16},{"key":{"Integer":{"Unsigned":"Usize"}},"value":8},{"key":{"Float":"F16"},"value":2},{"key":{"Float":"F32"},"value":4},{"key":{"Float":"F64"},"value":8},{"key":{"Float":"F128"},"value":16},{"key":"Char","value":4}]}}],"type_decls":[{"def_id":0,"item_meta":{"name":[{"Builtin":[{"Tuple":0},0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null}},"source_text":null,"attr_info":{"attributes":[],"inline":null,"rename":null,"public":false},"is_local":false,"started_from":false,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"src":{"Builtin":"Tuple"},"kind":"Opaque","layout":[{"key":"aarch64-apple-darwin","value":{"size":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","0"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":null},"align":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","1"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":null},"discriminator":{"Known":0},"inhabited":{"Untagged":"True"},"variant_layouts":[{"field_offsets":[],"inhabited":{"Untagged":"True"},"tagger":[]}],"repr":{"repr_algo":"Rust","align_modif":null,"transparent":false,"explicit_discr_type":null}}}],"ptr_metadata":"None"},{"def_id":14,"item_meta":{"name":[{"Ident":["core",0]},{"Ident":["option",0]},{"Ident":["Option",0]}],"span":{"Untagged":{"data":{"file_id":25,"beg":{"line":598,"col":0},"end":{"line":598,"col":18}},"generated_from_span":null}},"source_text":null,"attr_info":{"attributes":[{"DocComment":" The `Option` type. See [the module level documentation](self) for more."}],"inline":null,"rename":null,"public":true},"is_local":false,"started_from":false,"is_extern":false,"opacity":"Foreign","lang_item":"Option","diagnostic_item":"Option","has_errors":false},"generics":{"regions":[],"types":[{"index":0,"name":"T","variance":"Covariant"}],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"src":"Normal","kind":{"Enum":[{"id":0,"span":{"Untagged":{"data":{"file_id":25,"beg":{"line":602,"col":4},"end":{"line":602,"col":8}},"generated_from_span":null}},"attr_info":{"attributes":[{"DocComment":" No value."}],"inline":null,"rename":null,"public":true},"name":"None","fields":[],"discriminant":{"Signed":["Isize","0"]}},{"id":1,"span":{"Untagged":{"data":{"file_id":25,"beg":{"line":606,"col":4},"end":{"line":606,"col":8}},"generated_from_span":null}},"attr_info":{"attributes":[{"DocComment":" Some value of type `T`."}],"inline":null,"rename":null,"public":true},"name":"Some","fields":[{"span":{"Untagged":{"data":{"file_id":25,"beg":{"line":606,"col":55},"end":{"line":606,"col":56}},"generated_from_span":null}},"attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"name":"_0","is_positional":true,"ty":{"Untagged":{"TypeVar":{"Bound":[0,0]}}}}],"discriminant":{"Signed":["Isize","1"]}}]},"layout":[{"key":"aarch64-apple-darwin","value":{"size":{"chosen":null,"guarantee":null},"align":{"chosen":null,"guarantee":null},"discriminator":null,"inhabited":{"Untagged":{"Or":[{"Untagged":{"And":[]}},{"Untagged":{"And":[{"Untagged":{"GenericType":{"Untagged":{"TypeVar":{"Bound":[0,0]}}}}}]}}]}},"variant_layouts":[{"field_offsets":[],"inhabited":{"Untagged":{"And":[]}},"tagger":[]},{"field_offsets":[{"guarantee":null,"chosen":null}],"inhabited":{"Untagged":{"And":[{"Untagged":{"GenericType":{"Untagged":{"TypeVar":{"Bound":[0,0]}}}}}]}},"tagger":[]}],"repr":{"repr_algo":"Rust","align_modif":null,"transparent":false,"explicit_discr_type":null}}}],"ptr_metadata":"None"},{"def_id":17,"item_meta":{"name":[{"Builtin":["Str",0]}],"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null}},"source_text":null,"attr_info":{"attributes":[],"inline":null,"rename":null,"public":false},"is_local":false,"started_from":false,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"src":{"Builtin":"Str"},"kind":{"Struct":[{"span":{"Untagged":{"data":{"file_id":0,"beg":{"line":1,"col":0},"end":{"line":1,"col":0}},"generated_from_span":null}},"attr_info":{"attributes":[],"inline":null,"rename":null,"public":true},"name":"_0","is_positional":true,"ty":{"Untagged":{"Slice":[{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}},null]}}}]},"layout":[{"key":"aarch64-apple-darwin","value":{"size":{"chosen":{"Untagged":{"FromMetadata":"SliceLength"}},"guarantee":null},"align":{"chosen":{"Untagged":{"Constant":{"Untagged":[{"Integer":{"Unsigned":["Usize","1"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"Usize"}}}}]}}},"guarantee":null},"discriminator":{"Known":0},"inhabited":{"Untagged":"True"},"variant_layouts":[],"repr":{"repr_algo":"Rust","align_modif":null,"transparent":false,"explicit_discr_type":null}}}],"ptr_metadata":"None"}],"fun_decls":[{"def_id":83,"item_meta":{"name":[{"Ident":["zerocopy",0]},{"Ident":["util",0]},{"Ident":["safety_checks",0]},{"Ident":["checked_bool",0]}],"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":28,"col":0},"end":{"line":38,"col":1}},"generated_from_span":null}},"source_text":"fn checked_bool(byte: u8) -> Option {\n if byte < 2 {\n // SAFETY: The branch restricts `byte` to 0 or 1, the two boolean bit\n // patterns. Both types have size one, satisfying the helper's size\n // assertion. The trusted interpretation checks this same condition\n // before producing a bool; it cannot silently accept another byte.\n Some(unsafe { super::transmute_unchecked(byte) })\n } else {\n None\n }\n}","attr_info":{"attributes":[{"DocComment":" Converts precisely the two valid boolean encodings."},{"DocComment":""},{"DocComment":" ```aeneas"},{"DocComment":" spec checked_bool_spec"},{"DocComment":" ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none"},{"DocComment":" ```"}],"inline":null,"rename":null,"public":false},"is_local":true,"started_from":true,"is_extern":false,"opacity":"Transparent","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"signature":{"is_unsafe":false,"abi":"Rust","is_variadic":false,"inputs":[{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}],"output":{"Untagged":{"Adt":{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null}}}},"src":"Normal","body":{"Unstructured":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":28,"col":0},"end":{"line":38,"col":1}},"generated_from_span":null}},"bound_body_regions":0,"locals":{"arg_count":1,"locals":[{"index":0,"name":null,"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":28,"col":29},"end":{"line":28,"col":41}},"generated_from_span":null}},"ty":{"Untagged":{"Adt":{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null}}},"drop_flag_for":null},{"index":1,"name":"byte","span":{"Untagged":{"data":{"file_id":18,"beg":{"line":28,"col":16},"end":{"line":28,"col":20}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}},"drop_flag_for":null},{"index":2,"name":null,"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":15}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":"Bool"}},"drop_flag_for":null},{"index":3,"name":null,"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":11}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}},"drop_flag_for":null},{"index":4,"name":null,"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":13},"end":{"line":34,"col":56}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":"Bool"}},"drop_flag_for":null},{"index":5,"name":null,"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":49},"end":{"line":34,"col":53}},"generated_from_span":null}},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}},"drop_flag_for":null}]},"body":[{"statements":[{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":15}},"generated_from_span":null}},"kind":{"StorageLive":2},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":11}},"generated_from_span":null}},"kind":{"StorageLive":3},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":11}},"generated_from_span":null}},"kind":{"Assign":[{"kind":{"Local":3},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}},{"Use":[{"Copy":{"kind":{"Local":1},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}}},"Yes"]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":15}},"generated_from_span":null}},"kind":{"Assign":[{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":"Bool"}}},{"BinaryOp":["Lt",{"Move":{"kind":{"Local":3},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}}},{"Const":{"Untagged":[{"Integer":{"Unsigned":["U8","2"]}},{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}]}}]}]},"comments_before":[]}],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":7},"end":{"line":29,"col":15}},"generated_from_span":null}},"kind":{"Switch":{"data":{"scrutinee":{"Value":{"Move":{"kind":{"Local":2},"ty":{"Untagged":{"Scalar":"Bool"}}}}},"branches":[[{"Untagged":[{"Bool":false},{"Untagged":{"Scalar":"Bool"}}]},1]],"fallback":0},"branches":[1,2]}},"comments_before":[]}},{"statements":[{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":14},"end":{"line":29,"col":15}},"generated_from_span":null}},"kind":{"StorageDead":3},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":13},"end":{"line":34,"col":56}},"generated_from_span":null}},"kind":{"StorageLive":4},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":49},"end":{"line":34,"col":53}},"generated_from_span":null}},"kind":{"StorageLive":5},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":49},"end":{"line":34,"col":53}},"generated_from_span":null}},"kind":{"Assign":[{"kind":{"Local":5},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}},{"Use":[{"Copy":{"kind":{"Local":1},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}}},"Yes"]}]},"comments_before":[]}],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":22},"end":{"line":34,"col":54}},"generated_from_span":null}},"kind":{"Call":{"call":{"func":{"Regular":{"kind":{"Fun":145},"generics":{"regions":[],"types":[{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}},{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]}}},"args":[{"Move":{"kind":{"Local":5},"ty":{"Untagged":{"Scalar":{"Integer":{"Unsigned":"U8"}}}}}}],"dest":{"kind":{"Local":4},"ty":{"Untagged":{"Scalar":"Bool"}}}},"target":4,"on_unwind":3}},"comments_before":[]}},{"statements":[{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":14},"end":{"line":29,"col":15}},"generated_from_span":null}},"kind":{"StorageDead":3},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":36,"col":8},"end":{"line":36,"col":12}},"generated_from_span":null}},"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Adt":{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null}}}},{"Aggregate":[{"Adt":[{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null},0,null]},[]]}]},"comments_before":[]}],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":4},"end":{"line":37,"col":5}},"generated_from_span":null}},"kind":{"Goto":{"target":5}},"comments_before":[]}},{"statements":[],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":28,"col":0},"end":{"line":38,"col":1}},"generated_from_span":null}},"kind":"UnwindResume","comments_before":[]}},{"statements":[{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":53},"end":{"line":34,"col":54}},"generated_from_span":null}},"kind":{"StorageDead":5},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":8},"end":{"line":34,"col":57}},"generated_from_span":null}},"kind":{"Assign":[{"kind":{"Local":0},"ty":{"Untagged":{"Adt":{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null}}}},{"Aggregate":[{"Adt":[{"id":14,"generics":{"regions":[],"types":[{"Untagged":{"Scalar":"Bool"}}],"const_generics":[],"trait_refs":[]},"builtin":null},1,null]},[{"Move":{"kind":{"Local":4},"ty":{"Untagged":{"Scalar":"Bool"}}}}]]}]},"comments_before":[]},{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":34,"col":56},"end":{"line":34,"col":57}},"generated_from_span":null}},"kind":{"StorageDead":4},"comments_before":[]}],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":29,"col":4},"end":{"line":37,"col":5}},"generated_from_span":null}},"kind":{"Goto":{"target":5}},"comments_before":[]}},{"statements":[{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":37,"col":4},"end":{"line":37,"col":5}},"generated_from_span":null}},"kind":{"StorageDead":2},"comments_before":[]}],"terminator":{"span":{"Untagged":{"data":{"file_id":18,"beg":{"line":38,"col":1},"end":{"line":38,"col":1}},"generated_from_span":null}},"kind":"Return","comments_before":[]}}],"comments":[[34,["SAFETY: The branch restricts `byte` to 0 or 1, the two boolean bit","patterns. Both types have size one, satisfying the helper's size","assertion. The trusted interpretation checks this same condition","before producing a bool; it cannot silently accept another byte."]]]}}},{"def_id":145,"item_meta":{"name":[{"Ident":["zerocopy",0]},{"Ident":["util",0]},{"Ident":["transmute_unchecked",0]}],"span":{"Untagged":{"data":{"file_id":15,"beg":{"line":344,"col":0},"end":{"line":373,"col":1}},"generated_from_span":null}},"source_text":"pub(crate) const unsafe fn transmute_unchecked(src: Src) -> Dst {\n static_assert!(Src, Dst => core::mem::size_of::() == core::mem::size_of::());\n\n #[repr(C)]\n union Transmute {\n src: ManuallyDrop,\n dst: ManuallyDrop,\n }\n\n // SAFETY: Since `Transmute` is `#[repr(C)]`, its `src` and `dst`\n // fields both start at the same offset and the types of those fields are\n // transparent wrappers around `Src` and `Dst` [1]. Consequently,\n // initializing `Transmute` with with `src` and then reading out `dst` is\n // equivalent to transmuting from `Src` to `Dst` [2]. Transmuting from `src`\n // to `Dst` is valid because \u2014 by contract on the caller \u2014 `src` is a valid\n // instance of `Dst`.\n //\n // [1] Per https://doc.rust-lang.org/1.82.0/std/mem/struct.ManuallyDrop.html:\n //\n // `ManuallyDrop` is guaranteed to have the same layout and bit\n // validity as `T`, and is subject to the same layout optimizations as\n // `T`.\n //\n // [2] Per https://doc.rust-lang.org/1.82.0/reference/items/unions.html#reading-and-writing-union-fields:\n //\n // Effectively, writing to and then reading from a union with the C\n // representation is analogous to a transmute from the type used for\n // writing to the type used for reading.\n unsafe { ManuallyDrop::into_inner(Transmute { src: ManuallyDrop::new(src) }.dst) }\n}","attr_info":{"attributes":[{"DocComment":" Unsafely transmutes the given `src` into a type `Dst`."},{"DocComment":""},{"DocComment":" # Safety"},{"DocComment":""},{"DocComment":" The value `src` must be a valid instance of `Dst`."},{"Builtin":{"Inline":["Always",{"Untagged":{"data":{"file_id":15,"beg":{"line":343,"col":0},"end":{"line":343,"col":17}},"generated_from_span":null}}]}}],"inline":"Always","rename":null,"public":false},"is_local":true,"started_from":false,"is_extern":false,"opacity":"Opaque","lang_item":null,"diagnostic_item":null,"has_errors":false},"generics":{"regions":[],"types":[{"index":0,"name":"Src","variance":"Contravariant"},{"index":1,"name":"Dst","variance":"Covariant"}],"const_generics":[],"trait_clauses":[],"regions_outlive":[],"types_outlive":[],"trait_type_constraints":[]},"signature":{"is_unsafe":true,"abi":"Rust","is_variadic":false,"inputs":[{"Untagged":{"TypeVar":{"Bound":[0,0]}}}],"output":{"Untagged":{"TypeVar":{"Bound":[0,1]}}}},"src":"Normal","body":"Opaque"}],"global_decls":[],"trait_decls":[],"trait_impls":[]}} diff --git a/verification/aeneas/tests/annotation-origins.sh b/verification/aeneas/tests/annotation-origins.sh new file mode 100755 index 0000000000..2771e851f9 --- /dev/null +++ b/verification/aeneas/tests/annotation-origins.sh @@ -0,0 +1,213 @@ +#!/usr/bin/env bash +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + + +# Exercise native HIR discovery independently of extraction reachability. Fixtures +# live in a private target directory and never alter the production source census. +set -euo pipefail +[[ $# == 0 ]] || { echo "Usage: $0" >&2; exit 1; } +: "${AENEAS_TOOLCHAIN_DIR:?Set AENEAS_TOOLCHAIN_DIR to the pinned patched runtime}" +cd "$(dirname "$0")/../../.." +repo=$PWD +source verification/aeneas/toolchain.sh +tools_dir=$AENEAS_TOOLCHAIN_DIR +export CARGO_NET_OFFLINE=true +mkdir -p "$repo/target/aeneas" +work=$(mktemp -d "$repo/target/aeneas/annotation-origins.XXXXXX") +trap 'status=$?; if [[ $status == 0 ]]; then rm -rf "$work"; else echo "Native origin control artifacts retained: $work" >&2; fi' EXIT +cat > "$work/origins.rs" <<'RUST' +#![allow(unused)] +unsafe trait Law {} +struct Ordinary; +/// ```aeneas +/// invariant_proof +/// ``` +unsafe impl Law for Ordinary {} +macro_rules! forward { ($(#[$doc:meta])* $ty:ty) => { $(#[$doc])* unsafe impl Law for $ty {} }; } +struct Forwarded; +forward! { + #[doc = " ```aeneas\n invariant_proof\n ```"] + Forwarded +} +macro_rules! duplicate { ($(#[$doc:meta])* $a:ty, $b:ty) => { $(#[$doc])* unsafe impl Law for $a {} $(#[$doc])* unsafe impl Law for $b {} }; } +struct First; struct Second; +duplicate! { + /// ```aeneas + /// invariant_proof + /// ``` + First, Second +} +struct Field { + /// ```aeneas + /// spec + /// ``` + value: u8, +} +/// function doc +fn included() {} +fn excluded() { + /// ```aeneas + /// spec + /// ``` + let local = 1; +} + +/// public const function doc +pub(crate) const fn with_modifiers() -> u8 { 0 } +/// public unsafe trait doc +pub unsafe trait PublicTrait {} +/// ```aeneas +/// model tuple struct +/// ``` +struct TupleModel(u8); +/// ```aeneas +/// model unit struct +/// ``` +struct UnitModel; +struct BadTupleField( + /// ```aeneas + /// model forbidden tuple field + /// ``` + u8, +); +enum BadVariant { + /// ```aeneas + /// model forbidden variant + /// ``` + Variant(u8), +} +RUST +python3 -B - "$tools_dir/charon" "$work" <<'PYTEST' +import json +import os +from pathlib import Path +import subprocess +import sys + +charon = Path(sys.argv[1]) +work = Path(sys.argv[2]) +fixture = work / 'origins.rs' +data = fixture.read_bytes() +steps = [] + + +def run(label, selector, source=fixture, diagnostic=None): + env = os.environ.copy() + # macOS protected interpreters may drop inherited DYLD variables. Restore + # the pinned runtime's library location inside the subprocess environment. + libraries = str(charon.parent / 'rust/lib') + env['DYLD_LIBRARY_PATH'] = libraries + ':' + str(charon.parent / 'libs') + env['LD_LIBRARY_PATH'] = libraries + ':' + str(charon.parent / 'libs') + env['CHARON_ANNOTATION_ORIGINS'] = str(work / (label + '.origins.json')) + env['CHARON_ADMISSION_SNAPSHOT'] = str(work / (label + '.before.ullbc')) + command = [ + str(charon), 'rustc', '--preset=aeneas', '--sysroot', 'default', + '--start-from', selector, '--mir', 'promoted', '--no-dedup-serialized-ast', + '--dest-file', str(work / (label + '.llbc')), '--abort-on-error', + '--error-on-warnings', '--', '--crate-name', 'native_origin', + '--crate-type', 'lib', source.name, + ] + result = subprocess.run(command, cwd=work, env=env, text=True, capture_output=True) + log = result.stdout + result.stderr + (work / (label + '.log')).write_text(log) + steps.append({'case': label, 'selector': selector, 'exit': result.returncode, + 'diagnostic': diagnostic, 'command': command}) + (work / 'commands.json').write_text(json.dumps(steps, indent=2) + '\n') + if diagnostic is not None: + assert result.returncode != 0 and diagnostic in log, (label, log) + return None + assert result.returncode == 0, (label, log) + return json.loads((work / (label + '.origins.json')).read_text()) + + +def origin(node): + doc = node['docs'][0] + return f"@doc-origin:{doc['file']}:{doc['begin']}:{doc['end']}" + + +# Every positive extraction must pass before any expected failure is attempted. +# Operational failures therefore cannot count as successful negative controls. +baseline = run('selected-function-census', 'native_origin::included') +assert baseline['version'] == 1 +nodes = baseline['nodes'] +impls = [node for node in nodes if node['node_kind'] == 'trait-impl'] +assert len(impls) == 4 and all(node['positive'] for node in impls), impls +assert all(node['trait_impl_id'] is None for node in impls), impls +assert next(source['text'] for source in baseline['sources'] + if source['file'] == fixture.name) == data.decode() + +# rustc aliases tuple/unit docs onto a synthetic ctor. Only that exact nominal +# compiler alias may be folded; independent field/variant/statement docs survive. +for name in ['TupleModel', 'UnitModel']: + owners = [node for node in nodes if node['owner'].endswith(name)] + assert len(owners) == 1 and owners[0]['node_kind'] == 'type', owners +for text in ['forbidden tuple field', 'forbidden variant']: + owners = [node for node in nodes if any(text in doc['text'] for doc in node['docs'])] + assert owners and all(node['node_kind'] == 'unsupported' for node in owners), owners +for marker in [b' value: u8,', b' let local = 1;']: + owners = [node for node in nodes if node['span']['begin'] == data.index(marker.lstrip())] + assert owners and all(node['node_kind'] == 'unsupported' for node in owners), owners + if marker == b' let local = 1;': + assert len(owners) == 2, owners # Both Stmt and LetStmt aliases are censused. +for name, start in [('with_modifiers', b'pub(crate) const fn'), + ('PublicTrait', b'pub unsafe trait')]: + node = next(node for node in nodes if node['owner'].endswith(name)) + assert node['span']['begin'] == data.index(start), node + +raw = next(node for node in impls + if any('invariant_proof' in doc['text'] and '\n' in doc['text'] + for doc in node['docs'])) +selected = run('macro-unique', origin(raw)) +selected_impl = next(node for node in selected['nodes'] if node['owner'] == raw['owner']) +impl_id = selected_impl['trait_impl_id'] +assert type(impl_id) is int +before = json.loads((work / 'macro-unique.before.ullbc').read_text()) +final = json.loads((work / 'macro-unique.llbc').read_text()) +assert selected_impl['trait_impl'] == before['translated']['trait_impls'][impl_id] +assert final['translated']['trait_impls'][impl_id] is not None +ordinary = next(node for node in impls + if node['span']['begin'] == data.index(b'unsafe impl Law for Ordinary')) +run('direct-doc-origin', origin(ordinary)) +span = ordinary['span'] +run('span-preserved', f"@span:{span['file']}:{span['begin']}:{span['end']}") + +# Value spans and sugared comment spans use physical byte positions even though +# rustc's captured source text has normalized CRLF and removed the leading BOM. +bom = work / 'bom-crlf.rs' +bom_data = ('\ufeff#![allow(unused)]\r\nunsafe trait Law {}\r\nstruct Bytes;\r\n' + '/// ```aeneas\r\n/// invariant_proof\r\n/// ```\r\n' + '#[doc = r#" literal é"#]\r\nunsafe impl Law for Bytes {}\r\n' + 'fn included() {}\r\n').encode() +bom.write_bytes(bom_data) +normalized = run('bom-crlf', 'native_origin::included', source=bom) +bom_impl = next(node for node in normalized['nodes'] if node['node_kind'] == 'trait-impl') +assert bom_impl['docs'][0]['begin'] == bom_data.index(b'/// ```aeneas') +literal = bom_impl['docs'][-1] +spelling = 'r#" literal é"#'.encode() +assert literal['begin'] == bom_data.index(spelling) +assert literal['end'] == literal['begin'] + len(spelling) +assert literal['text'] == ' literal é' +assert next(source['text'] for source in normalized['sources'] + if source['file'] == bom.name) == bom_data.decode('utf-8-sig').replace('\r\n', '\n') + +# Repeated forwarding remains two distinct native owners, so selecting its +# shared fragment must fail with a cardinality diagnostic. A missing fragment +# must fail semantically too; compiler startup errors do not satisfy either test. +counts = {} +for node in impls: + for doc in node['docs']: + counts.setdefault((doc['file'], doc['begin'], doc['end']), []).append(node) +duplicated = next(owners for owners in counts.values() if len(owners) == 2) +assert len({node['owner'] for node in duplicated}) == 2 +run('duplicate-rejected', origin(duplicated[0]), + diagnostic='matched 2 positive local trait impls; expected exactly one') +run('missing-rejected', f'@doc-origin:{fixture.name}:1:2', + diagnostic='matched 0 positive local trait impls; expected exactly one') +print('Native annotation-origin controls passed (5 positive extractions, 2 semantic failures)') +PYTEST diff --git a/verification/aeneas/tests/provided_method_controls.py b/verification/aeneas/tests/provided_method_controls.py new file mode 100644 index 0000000000..e723994b31 --- /dev/null +++ b/verification/aeneas/tests/provided_method_controls.py @@ -0,0 +1,121 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Regression for excluded provided signatures and actual method references. + +Usage: provided-method-controls.py CHARON OUTPUT_DIR REPO_ROOT RUST_LIBRARY_DIR +The runtime supplies the pinned Rust executable on PATH. Every output is private +scratch; existing output names reject rather than overwrite another run. +""" + +import json +import os +from pathlib import Path +import subprocess +import sys + + +def check(charon, output, repo, libraries): + output.mkdir(parents=True, exist_ok=True) + source = Path(__file__).with_suffix('.rs') + results = [] + for case in ['keep', 'concrete_keep', 'override_keep', 'required_excluded', + 'generic_call', 'concrete_call', 'override_call', 'through_hidden', 'inherent_call']: + prefix = output / case + if any(Path(str(prefix) + suffix).exists() for suffix in ('.log', '.llbc', '.before.ullbc')): + raise AssertionError('Compiler regression outputs already exist: ' + str(prefix)) + selected = 'keep' if case == 'required_excluded' else case + env = os.environ.copy() + for variable in ['DYLD_LIBRARY_PATH', 'LD_LIBRARY_PATH']: + env[variable] = str(libraries) + (':' + env[variable] if env.get(variable) else '') + env['CHARON_ADMISSION_SNAPSHOT'] = str(prefix) + '.before.ullbc' + options = ['--exclude', 'provided_method_controls::Api::unused', + '--exclude', 'provided_method_controls::Api::called'] + if case == 'required_excluded': + options += ['--exclude', 'provided_method_controls::Api::required'] + if case == 'inherent_call': + options += ['--exclude', 'provided_method_controls::Plain::plain'] + if case == 'through_hidden': + options += ['--opaque', 'provided_method_controls::hidden_call'] + command = [str(charon), 'rustc', '--preset=aeneas', '--sysroot', 'default', + '--start-from', 'provided_method_controls::' + selected, + '--mir', 'promoted', '--no-dedup-serialized-ast', *options, + '--dest-file', str(prefix) + '.llbc', '--abort-on-error', + '--error-on-warnings', '--', '--crate-name', 'provided_method_controls', + '--crate-type', 'lib', str(source)] + result = subprocess.run(command, env=env, text=True, capture_output=True, cwd=output) + text = result.stdout + result.stderr + Path(str(prefix) + '.log').write_text(text) + record = {'case': case, 'command': command, 'exit_code': result.returncode} + results.append(record) + if case in ['generic_call', 'concrete_call', 'override_call']: + if result.returncode == 0 or 'referenced excluded provided trait method' not in text: + raise AssertionError('Excluded method reference was accepted or rejected for the wrong reason: ' + case) + continue + if result.returncode != 0: + raise AssertionError('Malformed positive extraction: ' + case + '\n' + text) + for suffix in ('.llbc', '.before.ullbc'): + data = json.loads(Path(str(prefix) + suffix).read_text()) + if data.get('has_errors') is not False: + raise AssertionError('Extraction reported errors: ' + case + suffix) + crate = data['translated'] + if case == 'inherent_call': + # This fix governs provided trait slots; an excluded inherent + # method retains upstream extraction behavior and is not admitted. + continue + traits = {t['def_id']: t for t in crate['trait_decls'] if t} + names = {i: t['item_meta']['name'][-1].get('Ident', [None])[0] + for i, t in traits.items()} + if 'OnlyUnusedDependency' in names.values(): + raise AssertionError('Unused provided signature imported its dependency') + api = [t for t in traits.values() if names[t['def_id']] == 'Api'] + if len(api) != 1: + raise AssertionError('Missing exact Api declaration') + methods = api[0]['methods'] + slots = [(i, m) for i, m in enumerate(methods) if m is not None] + if len(slots) != 1 or slots[0][0] != 1: + raise AssertionError('Required original method slot was lost or renumbered') + method = slots[0][1] + if (method['skip_binder']['name'] != 'required' + or method['kind'] != {'TraitMethod': [api[0]['def_id'], 1]}): + raise AssertionError('Required method changed compiler identity') + bounds = method['params']['trait_clauses'] + if not any(names[b['trait_']['skip_binder']['id']] == 'RequiredDependency' for b in bounds): + raise AssertionError('Required method signature lost its original bound') + if case == 'through_hidden': + sys.path.insert(0, str(repo / 'verification/aeneas')) + import admission + hidden = next(f for f in crate['fun_decls'] if f and + f['item_meta']['name'][-1].get('Ident') == ['hidden_call', 0]) + if hidden['body'] != 'Opaque': + raise AssertionError('Opaque-helper control did not exercise an opaque body') + # Exercise the existing body-boundary guard on the actual emitted record. + # This unit test intentionally does not claim whole-profile admission; + # the production profile separately rejects this extra opaque selection. + audit = admission.Admission.__new__(admission.Admission) + audit.crate = crate + audit.functions = {f['def_id']: f for f in crate['fun_decls'] if f} + audit.types = {t['def_id']: t for t in crate['type_decls'] if t} + audit.registry = [] + audit.visited = {} + audit.checked_types = set() + audit.before = suffix == '.before.ullbc' + try: + audit.visit(hidden['def_id']) + except ValueError as error: + if str(error) != 'No reviewed interpretation for provided_method_controls::hidden_call': + raise AssertionError('Unintended opaque boundary rejection: ' + str(error)) from error + else: + raise AssertionError('Unreviewed opaque helper was accepted') + return results + + +if __name__ == '__main__': + if len(sys.argv) != 5: + raise SystemExit(__doc__) + print(json.dumps(check(*(Path(arg).resolve() for arg in sys.argv[1:])), indent=2)) diff --git a/verification/aeneas/tests/provided_method_controls.rs b/verification/aeneas/tests/provided_method_controls.rs new file mode 100644 index 0000000000..57e1c0a832 --- /dev/null +++ b/verification/aeneas/tests/provided_method_controls.rs @@ -0,0 +1,75 @@ +// Copyright 2026 The Fuchsia Authors +// +// Licensed under a BSD-style license , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +#![allow(dead_code)] +trait OnlyUnusedDependency { + fn unused_dependency(&self); +} +trait RequiredDependency { + fn required_dependency(&self); +} +trait Api { + // Slot zero is omitted, so retaining the required slot must preserve a gap. + fn unused(&self, value: T) { + value.unused_dependency(); + } + fn required(&self, value: T) -> T; + fn called(&self) -> u8 { + 9 + } +} +impl Api for u8 { + fn required(&self, value: T) -> T { + value + } +} +impl Api for u16 { + fn required(&self, value: T) -> T { + value + } + fn unused(&self, value: T) { + value.unused_dependency(); + } + fn called(&self) -> u8 { + 10 + } +} +fn keep(value: T) -> T { + value +} +fn concrete_keep(value: u8) -> u8 { + keep(value) +} +fn override_keep(value: u16) -> u16 { + keep(value) +} +fn generic_call(value: T) -> u8 { + value.called() +} +fn concrete_call(value: u8) -> u8 { + value.called() +} +fn override_call(value: u16) -> u8 { + value.called() +} +fn hidden_call(value: T) -> u8 { + value.called() +} +fn through_hidden(value: u8) -> u8 { + hidden_call(value) +} + +struct Plain; +impl Plain { + fn plain() -> u8 { + 7 + } +} +fn inherent_call() -> u8 { + Plain::plain() +} diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py new file mode 100644 index 0000000000..dec9cac8f6 --- /dev/null +++ b/verification/aeneas/tests/test_admission.py @@ -0,0 +1,189 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Mutate a real pinned pre-transformation extraction, preserving each cause. + +These controls do not execute invalid Rust. Admission failures are separate +from the kernel tests of the guarded primitives and their caller contracts. +""" +import copy +import json +import os +from pathlib import Path +import sys +import tempfile +import unittest +from unittest import mock + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import admission + + +class AdmissionTests(unittest.TestCase): + def setUp(self): + self.data = json.loads((Path(__file__).with_name('admission') / + 'boolean.before.ullbc').read_text()) + # The preserved fixture predates interface-only IntoBytes extraction. + # Only unused provided methods can be excluded; any executable reference + # is a compiler error, also covered by native front-end controls. + self.data['translated']['options']['exclude'] = list(admission.EXCLUDED_PROVIDED_METHODS) + self.registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) + self.root = 'zerocopy::util::safety_checks::checked_bool' + + def check(self): + return admission.Admission(self.data, self.registry).audit([self.root]) + + def body(self): + return self.data['translated']['fun_decls'][0]['body']['Unstructured']['body'] + + def test_transitive_registered_boundary(self): + report = self.check() + self.assertEqual(report['roots'], [self.root]) + self.assertIn('zerocopy::util::transmute_unchecked', + [row['rust'] for row in report['executions']]) + + def test_unreviewed_exclusions_fail_closed(self): + for exclusions in ([], [*admission.EXCLUDED_PROVIDED_METHODS, 'zerocopy::unsafe_helper']): + self.data['translated']['options']['exclude'] = exclusions + with self.assertRaisesRegex(ValueError, 'Unreviewed extraction option exclude'): + self.check() + + def test_missing_registration_is_not_an_opaque_success(self): + self.registry = [r for r in self.registry if not r.get('opaque')] + self.data['translated']['options']['opaque'] = [] + with self.assertRaisesRegex(ValueError, 'No reviewed interpretation'): + self.check() + + def test_callee_annotations_never_exempt_unsupported_effects(self): + # This callee has a valid-looking proof comment, but no registered + # interpretation. Inspecting the caller must still reject its assembly. + callee = self.data['translated']['fun_decls'][1] + self.registry = [r for r in self.registry if not r.get('opaque')] + self.data['translated']['options']['opaque'] = [] + callee['item_meta']['attr_info']['attributes'] = [{'DocComment': '```aeneas'}] + callee['body'] = copy.deepcopy(self.data['translated']['fun_decls'][0]['body']) + callee['body']['Unstructured']['body'][0]['terminator']['kind'] = {'InlineAsm': { + 'asm': '', 'kind': 'Normal', 'targets': [], 'on_unwind': 0}} + with self.assertRaisesRegex(ValueError, 'InlineAsm'): + self.check() + + def test_unsupported_instantiation_even_with_same_named_boundary(self): + for block in self.body(): + call = block['terminator']['kind'] + if isinstance(call, dict) and 'Call' in call: + types = call['Call']['call']['func']['Regular']['generics']['types'] + types[0] = {'Untagged': {'Scalar': {'Integer': {'Unsigned': 'U16'}}}} + with self.assertRaisesRegex(ValueError, 'Unsupported transmute instantiation'): + self.check() + + def test_drop_before_cleanup_and_on_unwind_is_rejected(self): + for index in [0, len(self.body()) - 1]: + with self.subTest(block=index): + previous = self.body()[index]['terminator']['kind'] + self.body()[index]['terminator']['kind'] = {'Drop': {}} + with self.assertRaisesRegex(ValueError, 'original terminator Drop'): + self.check() + self.body()[index]['terminator']['kind'] = previous + + def test_new_operations_attributes_and_configuration_fail_closed(self): + original = copy.deepcopy(self.data) + mutations = [ + lambda: self.body()[0]['statements'].append({ + 'span': None, 'comments_before': [], 'kind': {'NewEffect': 0}}), + lambda: self.data['translated']['fun_decls'][0]['item_meta']['attr_info']['attributes'].append( + {'Unknown': {'path': 'target_feature', 'args': 'enable="x"'}}), + lambda: self.data['translated']['options'].update(skip_borrowck=True), + lambda: self.data['translated']['options'].update(new_erasure=True), + lambda: self.data['translated']['options'].update(ops_to_function_calls=False), + lambda: self.data['translated']['fun_decls'][0]['item_meta']['attr_info']['attributes'].append( + {'NewAttribute': None}), + lambda: self.data['translated']['target_information'][0]['value'].update(target_pointer_size=4), + ] + for mutate in mutations: + self.data = copy.deepcopy(original) + mutate() + with self.assertRaises(ValueError): + self.check() + + def test_padding_and_raw_storage_cannot_be_logical_values(self): + self.data['translated']['fun_decls'][0]['body']['Unstructured']['locals']['locals'][0]['ty'] = { + 'Untagged': {'RawPtr': []}} + with self.assertRaisesRegex(ValueError, 'raw pointers and storage'): + self.check() + + def test_bit_invalid_production_cannot_be_an_infallible_cast(self): + self.body()[0]['statements'].append({ + 'span': None, 'comments_before': [], 'kind': {'Assign': [ + {'kind': {'Local': 0}, 'ty': {'Untagged': {'Scalar': 'Bool'}}}, + {'UnaryOp': [{'Cast': {'Transmute': []}}, {'Const': None}]}]}}) + with self.assertRaisesRegex(ValueError, 'Unreviewed cast Transmute'): + self.check() + + def test_ub_abort_must_not_become_unwind_termination(self): + self.body()[0]['terminator']['kind'] = {'Abort': 'UnwindTerminate'} + with self.assertRaisesRegex(ValueError, 'Unreviewed abort UnwindTerminate'): + self.check() + + def test_guarded_translation_must_remain_failure_capable(self): + evidence = {'stages': {'llbc': {'executions': [ + {'rust': 'zerocopy::util::transmute_unchecked', + 'lean': 'util.transmute_unchecked'}]}}} + with tempfile.TemporaryDirectory() as directory: + work = Path(directory) + (work / 'Zerocopy').mkdir() + template = work / 'Zerocopy/FunsExternal_Template.lean' + signature = 'axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst' + template.write_text(signature) + admission.check_translation(work, evidence) + for mutant in [signature.replace('Result Dst', 'Dst'), '']: + template.write_text(mutant) + with self.assertRaisesRegex(ValueError, 'failure-capable signature'): + admission.check_translation(work, evidence) + + def test_compiler_override_is_rejected_before_compilation(self): + with mock.patch.dict(os.environ, RUSTFLAGS='-Zmir-opt-level=2'): + with self.assertRaisesRegex(ValueError, 'compiler override RUSTFLAGS'): + admission.input_identity(ROOT) + + def test_input_identity_covers_the_full_source_tree_and_shared_models(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + tools = root / 'runtime' + tools.mkdir() + (tools / 'aeneas-build.json').write_text('{}') + (root / 'zerocopy/src').mkdir(parents=True) + (root / 'zerocopy/src/lib.rs').write_text('fn f() {}') + with mock.patch.dict(os.environ, {'AENEAS_TOOLCHAIN_DIR': str(tools), + 'CARGO_HOME': str(root / 'cargo')}, clear=True): + baseline = admission.input_identity(root) + for name in ('zerocopy/src/vendor/new.rs', 'zerocopy/src/.lake/new.rs', + 'zerocopy/Cargo.lock', 'tools/aeneas-inline/Cargo.toml', + 'anneal/lean/Rust/Layout.lean', 'anneal/lean/golden/Model.lean', + 'anneal/flake.nix'): + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text('new verification input') + with self.subTest(name=name): + self.assertNotEqual(admission.input_identity(root), baseline) + path.unlink() + self.assertEqual(admission.input_identity(root), baseline) + for name in ('golden/Funs.lean', 'projections/Specs.lean'): + path = root / 'verification/aeneas' / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text('reviewed output') + self.assertEqual(admission.input_identity(root), baseline) + + def test_snapshot_is_mandatory(self): + with tempfile.TemporaryDirectory() as directory: + with self.assertRaisesRegex(ValueError, 'Missing mandatory before'): + admission.inspect(ROOT, Path(directory), [self.root], 'source-digest') + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index 566b8b0536..927b1ef31e 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -13,6 +13,7 @@ import sys import tempfile import unittest +from unittest import mock from pathlib import Path ROOT = Path(__file__).resolve().parents[3] @@ -66,6 +67,14 @@ def llbc(annotation, source): class InlineTests(unittest.TestCase): + def setUp(self): + patch = mock.patch('admission.inspect', return_value={'version': 1}) + patch.start() + self.addCleanup(patch.stop) + translation = mock.patch('admission.check_translation') + translation.start() + self.addCleanup(translation.stop) + def parse(self, source): return inline.parse_file(source, syntax(source)) diff --git a/verification/aeneas/tests/test_toolchain.py b/verification/aeneas/tests/test_toolchain.py index 2021899b50..cccaf96c3a 100644 --- a/verification/aeneas/tests/test_toolchain.py +++ b/verification/aeneas/tests/test_toolchain.py @@ -138,7 +138,8 @@ def test_cache_identity_invalidates_builder_archive_and_patch_changes(self): key = toolchain.cache_key(clone) self.assertEqual(key, toolchain.cache_key(ROOT)) for name in ['anneal/flake.lock', 'anneal/flake.nix', 'anneal/lean/Rust.lean', - 'verification/aeneas/build-aeneas.nix']: + 'verification/aeneas/build-aeneas.nix', + 'verification/aeneas/patches/admission-snapshot.patch']: target = clone / name original = target.read_bytes() target.write_bytes(original + b'\n') @@ -283,6 +284,8 @@ def frozen_directories(member): tar_script.chmod(0o755) artifact = scratch / 'patched-cli' artifact.mkdir() + for name in ('charon', 'charon-driver'): + shutil.copy2(self.tools / name, artifact / name) binary = artifact / 'aeneas' binary.write_text('#!/bin/sh\nif [ "$1" = -help ]; then echo -use-tuple-structs; else echo "aeneas ' + self.data['aeneas-release'] + toolchain.PATCH_SUFFIX + '"; fi\n') binary.chmod(0o755) @@ -365,6 +368,56 @@ def test_shell_exports_archive_cargo_and_versions(self): self.assertEqual(result.returncode, 0, result.stderr) self.assertEqual(result.stdout.splitlines(), [str(self.tools / 'rust/bin/cargo'), 'nightly-2099-01-01']) + def test_shell_exports_validated_runtime_for_admission_with_and_without_override(self): + root = Path(self.scratch.name) / 'project with spaces' + for name in ['anneal/flake.lock', 'verification/aeneas/toolchain.sh', + 'verification/aeneas/toolchain.py', 'verification/aeneas/admission.py', + 'verification/aeneas/source_inventory.py', + 'verification/aeneas/patches/use-tuple-structs.patch', + 'verification/aeneas/patches/admission-snapshot.patch']: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((ROOT / name).read_bytes()) + source = root / 'zerocopy/src/lib.rs' + source.parent.mkdir(parents=True) + source.write_text('fn f() {}\n') + default = root / 'target/aeneas/toolchain' + default.parent.mkdir(parents=True) + default.symlink_to(self.tools, target_is_directory=True) + child = ('import json,os,sys; from pathlib import Path; ' + 'sys.path.insert(0,"verification/aeneas"); import admission; ' + 'print(json.dumps({"tools":os.environ["AENEAS_TOOLCHAIN_DIR"],' + '"identity":admission.input_identity(Path.cwd())}))') + command = ('source verification/aeneas/toolchain.sh || exit; ' + + shlex.quote(sys.executable) + ' -B -c ' + shlex.quote(child)) + for override in (None, str(self.tools)): + with self.subTest(override=override): + env = dict(os.environ) + env.pop('AENEAS_TOOLCHAIN_DIR', None) + if override is not None: + env['AENEAS_TOOLCHAIN_DIR'] = override + result = subprocess.run(['bash', '-c', command], cwd=root, env=env, + capture_output=True, text=True) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + report = json.loads(result.stdout) + self.assertEqual(report['tools'], override or + str(root.resolve() / 'target/aeneas/toolchain')) + self.assertEqual(report['identity']['runtime'], + toolchain.digest(self.tools / 'aeneas-build.json')) + self.assertTrue(report['identity']['project']) + # Exporting the directory must not bypass archive validation. + record = self.tools / 'aeneas-build.json' + original = record.read_bytes() + try: + record.write_text('{}') + rejected = subprocess.run(['bash', '-c', command], cwd=root, env=env, + capture_output=True, text=True) + self.assertNotEqual(rejected.returncode, 0) + self.assertIn('provenance mismatch', rejected.stderr) + self.assertEqual(rejected.stdout, '') + finally: + record.write_bytes(original) + def test_shell_lake_policy_preserves_ci_and_failure_status(self): for status in (0, 19): with self.subTest(status=status): diff --git a/verification/aeneas/tests/test_workspace.py b/verification/aeneas/tests/test_workspace.py index dafa867cd0..9e65e3a02e 100644 --- a/verification/aeneas/tests/test_workspace.py +++ b/verification/aeneas/tests/test_workspace.py @@ -117,6 +117,93 @@ def test_incremental_development_rejects_a_proof_after_an_import_changes(self): with self.assertRaises(subprocess.CalledProcessError): workspace.develop(root, root, ['Proof']) + def test_ci_verification_cannot_accept_development_bindings(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for mode in (None, 'development', 'verified', ''): + (root / 'bindings.json').write_text(json.dumps({'mode': mode})) + with self.subTest(mode=mode), mock.patch.object(workspace, 'run_checked') as run: + with self.assertRaisesRegex(ValueError, 'CI verification requires verified-live'): + workspace.check(root, root, require_admission=True) + run.assert_not_called() + + def test_verified_check_requires_both_admission_stages_and_fresh_inputs(self): + # These are acceptance-path controls: no proof compilation may start + # when admission is absent, incomplete, stale, or bound to other roots. + import copy + import admission + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + work = root / 'project' + work.mkdir() + manifest = {'mode': 'verified-live', 'sources': 'source', + 'bindings': {'crate::f': {'kind': 'function'}}, + 'admission': {'version': 1, 'sources': 'source', + 'registry': 'registry', 'inputs': {'project': 'current'}, + 'stages': {stage: {'roots': ['crate::f']} + for stage in ('before', 'llbc')}}} + mutants = [] + mutant = copy.deepcopy(manifest) + del mutant['admission'] + mutants.append(mutant) + for stage in ('before', 'llbc'): + mutant = copy.deepcopy(manifest) + del mutant['admission']['stages'][stage] + mutants.append(mutant) + mutant = copy.deepcopy(manifest) + mutant['admission']['stages'][stage]['roots'] = [] + mutants.append(mutant) + for key, value in [('sources', 'other'), ('registry', 'other'), + ('inputs', {'project': 'old'})]: + mutant = copy.deepcopy(manifest) + mutant['admission'][key] = value + mutants.append(mutant) + with mock.patch.object(admission, 'input_identity', return_value={'project': 'current'}), \ + mock.patch.object(admission, 'digest', return_value='registry'), \ + mock.patch.object(workspace, 'run_checked') as run: + for mutant in mutants: + (work / 'bindings.json').write_text(json.dumps(mutant)) + with self.subTest(mutant=mutant), self.assertRaisesRegex(ValueError, 'admission evidence'): + workspace.check(root, work) + run.assert_not_called() + (work / 'bindings.json').write_text(json.dumps(manifest)) + workspace.check(root, work) + self.assertEqual(run.call_count, 3) + run.reset_mock() + # An editor changing Rust during a successful proof build must + # prevent that build from certifying the edited source. + with mock.patch.object(admission, 'input_identity', + side_effect=[{'project': 'current'}, {'project': 'edited'}]): + with self.assertRaisesRegex(ValueError, 'Inputs changed during proof'): + workspace.check(root, work) + self.assertEqual(run.call_count, 3) + run.reset_mock() + # Fresh extraction fingerprints do not establish freshness of + # the Lean sources copied before those fingerprints were made. + source = root / 'verification/aeneas/lean/Helper.lean' + source.parent.mkdir(parents=True) + source.write_text('def helper : Nat := 1\n') + copied = work / 'Helper.lean' + for contents in (None, 'def helper : Nat := 0\n'): + if contents is not None: + copied.write_text(contents) + with self.subTest(contents=contents), self.assertRaisesRegex( + ValueError, 'CI proof source differs'): + workspace.check(root, work, require_admission=True) + run.assert_not_called() + copied.write_bytes(source.read_bytes()) + workspace.check(root, work, require_admission=True) + self.assertEqual(run.call_count, 3) + run.reset_mock() + # A change to a copied source during compilation is also an + # editor experiment, not verification of the checkout. + def edit_copy(*_args): + copied.write_text('def helper : Nat := 2\n') + run.side_effect = edit_copy + with self.assertRaisesRegex(ValueError, 'CI proof source differs'): + workspace.check(root, work, require_admission=True) + self.assertEqual(run.call_count, 3) + def test_check_rejects_proof_cached_against_an_earlier_model(self): lake = shutil.which('lake') if lake is None: diff --git a/verification/aeneas/toolchain.py b/verification/aeneas/toolchain.py index bf4fb2a470..49ac6dd3d9 100644 --- a/verification/aeneas/toolchain.py +++ b/verification/aeneas/toolchain.py @@ -68,7 +68,12 @@ def publish_installation(source, destination): def build_identity(repo): """Bind the archive producer and patched builder, without adding upstream pins.""" - files = ['anneal/flake.lock', 'anneal/flake.nix', 'anneal/v1/Cargo.toml', 'anneal/rewrite-lake-vendor.py', 'anneal/prune-lake-cache.py', 'verification/aeneas/build-aeneas.nix', 'verification/aeneas/build-aeneas.sh', 'verification/aeneas/setup.sh', 'verification/aeneas/toolchain.py', 'verification/aeneas/patches/use-tuple-structs.patch'] + files = ["anneal/flake.lock", "anneal/flake.nix", "anneal/v1/Cargo.toml", + "anneal/rewrite-lake-vendor.py", "anneal/prune-lake-cache.py", + "verification/aeneas/build-aeneas.nix", "verification/aeneas/build-aeneas.sh", + "verification/aeneas/setup.sh", "verification/aeneas/toolchain.py", + "verification/aeneas/patches/use-tuple-structs.patch", + "verification/aeneas/patches/admission-snapshot.patch"] lean_root = repo / "anneal/lean" # The companion manifest is generated with checkout-specific paths. The # authoritative top-level manifest remains an archive build input. @@ -180,7 +185,9 @@ def probe(tools, data, patched): def provenance(tools, data, repo=None): result = {"metadata": data, "source_rev": data["aeneas-revision"], "source_nar_hash": data["aeneas-source-nar-hash"], - "patch_sha256": PATCH_SHA256, "version": data["aeneas-release"] + PATCH_SUFFIX, + "patch_sha256": PATCH_SHA256, + "admission_patch_sha256": digest(Path(__file__).with_name("patches") / "admission-snapshot.patch"), + "version": data["aeneas-release"] + PATCH_SUFFIX, "binary_sha256": digest(tools / "aeneas"), "upstream_binary_sha256": digest(tools / "aeneas-upstream"), "runtime_binary_sha256": {name: digest(tools / name) for name in diff --git a/verification/aeneas/toolchain.sh b/verification/aeneas/toolchain.sh index 0de6a4a312..b13abae9fb 100644 --- a/verification/aeneas/toolchain.sh +++ b/verification/aeneas/toolchain.sh @@ -12,6 +12,7 @@ _aeneas_repo=$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd) _aeneas_tools=${AENEAS_TOOLCHAIN_DIR:-"$_aeneas_repo/target/aeneas/toolchain"} _aeneas_values=$(python3 -B "$_aeneas_repo/verification/aeneas/toolchain.py" shell "$_aeneas_tools") || return 1 eval "$_aeneas_values" +export AENEAS_TOOLCHAIN_DIR="$_aeneas_tools" export PATH="$_aeneas_tools/rust/bin:$_aeneas_tools/lean/bin:$PATH" export LEAN_SYSROOT="$_aeneas_tools/lean" export LD_LIBRARY_PATH="$_aeneas_tools/rust/lib:$_aeneas_tools/lean/lib:$_aeneas_tools/lean/lib/lean${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}" diff --git a/verification/aeneas/workspace.py b/verification/aeneas/workspace.py index 70c1e64a9c..d93c66458f 100644 --- a/verification/aeneas/workspace.py +++ b/verification/aeneas/workspace.py @@ -222,8 +222,27 @@ def develop(root, work, targets=()): print('Development feedback complete. Run run.sh for final golden/live verification.', flush=True) -def check(root, work): +def check(root, work, *, require_admission=False): """Rebuild local proofs, then audit their compiled declarations.""" + manifest = json.loads((work / 'bindings.json').read_text()) + # CI uses verify, not the editor's check command. A development manifest + # may support proof iteration, but cannot certify fresh Rust extraction. + if require_admission and manifest.get('mode') != 'verified-live': + raise ValueError('CI verification requires verified-live bindings and execution admission') + if require_admission: + check_source_copies(root, work) + if manifest.get('mode') == 'verified-live': + import admission + evidence = manifest.get('admission') + roots = sorted(name for name, binding in manifest['bindings'].items() + if binding['kind'] == 'function') + if (not isinstance(evidence, dict) or evidence.get('version') != 1 or + evidence.get('sources') != manifest.get('sources') or + evidence.get('registry') != admission.digest(root / 'verification/aeneas/external.json') or + evidence.get('inputs') != admission.input_identity(root) or + set(evidence.get('stages', {})) != {'before', 'llbc'} or + any(stage.get('roots') != roots for stage in evidence['stages'].values())): + raise ValueError('Missing or stale mandatory admission evidence; run fresh extraction') # --old preserves the archive's read-only dependency caches, but ignores # changed imports. A persistent editor project could therefore reuse a proof # checked against an earlier model. Even the direct axiom audit would accept @@ -250,16 +269,12 @@ def check(root, work): # sources again while reusing the immutable toolchain dependencies. # The audit also writes the proof graph; run it even when Lake caches imports. run_checked(['lake', 'env', 'lean', '-DwarningAsError=true', 'Check.lean'], root, work) - - -def verify(root, work): - """Verify the pre-admission stage's live binding and exact proof sources.""" - manifest = json.loads((work / 'bindings.json').read_text()) - if manifest.get('mode') != 'verified-live': - raise ValueError('CI verification requires verified-live bindings') - check_source_copies(root, work) - check(root, work) - check_source_copies(root, work) + if require_admission: + check_source_copies(root, work) + # Checking takes long enough for an editor to change the source mid-run. + # Such a run may help development, but it cannot certify the new source. + if manifest.get('mode') == 'verified-live' and evidence['inputs'] != admission.input_identity(root): + raise ValueError('Inputs changed during proof checking; run fresh extraction') def inspect_spec(root, work, spec): @@ -362,10 +377,8 @@ def main(): inspect_spec(root, work, args.spec) elif args.command == 'develop': develop(root, work, args.target) - elif args.command == 'verify': - verify(root, work) else: - check(root, work) + check(root, work, require_admission=args.command == 'verify') if __name__ == '__main__': diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index a493f48f70..a09045dccd 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -297,6 +297,10 @@ pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { /// Copies `src` into the prefix of `dst`. /// +/// Aeneas models this as a trusted byte-copy boundary registered in +/// `verification/aeneas/external.json`; it does not extract this pointer body. +/// The model checks the length guard and retains the updated destination. +/// /// # Safety /// /// The caller guarantees that `src.len() <= dst.len()`. @@ -320,6 +324,10 @@ pub(crate) unsafe fn copy_unchecked(src: &[u8], dst: &mut [u8]) { /// Unsafely transmutes the given `src` into a type `Dst`. /// +/// Aeneas admits only the `u8` to `bool` instantiation as a trusted boundary +/// registered in `verification/aeneas/external.json`. Its model checks bit +/// validity before constructing a Boolean; this union body is not extracted. +/// /// # Safety /// /// The value `src` must be a valid instance of `Dst`.