From 3934374b9b8ea06b8edeb0d727ac3972404d01fe Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 12:23:41 -0400 Subject: [PATCH] Record encountered Aeneas limitations and workarounds Collect the extraction and modeling obstacles encountered while verifying zerocopy, including resolved blockers and the restrictions enforced by our admission checks. For each area, explain the effect on verification, the available workaround, the supporting evidence, and useful upstream changes. Separate current-pin failures and source findings from older experiments and local integration policy. Include the historical research inventory and exact source checkpoints so another researcher can investigate without mistaking a past limitation for a current upstream defect. gherrit-pr-id: Gneejf7sfxfhlqt7uozlawy72qjlpsrv2 Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/AENEAS_LIMITATIONS.md | 1242 +++++++++++++++++++++ verification/aeneas/README.md | 3 + 2 files changed, 1245 insertions(+) create mode 100644 verification/aeneas/AENEAS_LIMITATIONS.md diff --git a/verification/aeneas/AENEAS_LIMITATIONS.md b/verification/aeneas/AENEAS_LIMITATIONS.md new file mode 100644 index 0000000000..2b37411999 --- /dev/null +++ b/verification/aeneas/AENEAS_LIMITATIONS.md @@ -0,0 +1,1242 @@ + + +# Aeneas limitations encountered while verifying zerocopy + +This report is a handoff for someone considering improvements to Aeneas and +Charon. It records the obstacles we encountered, the semantic information we +need, our workarounds, and the changes that would remove those workarounds. +It includes resolved obstacles because their solutions are part of the cost of +using the tools. A local restriction is not necessarily an upstream limitation. + +The central finding is that **functional extraction supports substantially more +of our arithmetic and value reasoning than it supports of the connection to +Rust execution**. Most difficult proof infrastructure establishes which source +operation a theorem describes, which conditions survived extraction, and which +unsafe effects the extraction may have omitted. A successful extraction and a +Lean proof do not, by themselves, establish that connection. + +## Scope, versions, and status + +This report was prepared on October 15, 2026. The authoritative upstream bases +used by the current stack are: + +| Component | Version | +| --- | --- | +| Aeneas | `ca282ec2312a96f6a985a4d23a663690816d3f3e` | +| Charon | `cf02e3f228f97ee7be3a415be56989053063326d` | +| Extraction compiler | `nightly-2026-09-17` | +| Lean | `4.31.0` | + +Anneal's lockfile supplies the pins. Our runtime adds the checked-in +[tuple-struct option patch](patches/use-tuple-structs.patch) and +[Charon admission/origin patch](patches/admission-snapshot.patch). It also applies +one narrow generated-field naming repair in [prepare.py](prepare.py). +Claims about upstream implementation below refer to these bases, not to current +upstream HEAD. No upstream upgrade was attempted for this report. + +The published source checkpoint used for this report is +`f1573e5f7307fde4522ad8ad94cf834f02386179`. +The generic `transmute_copy` extension described below is a subsequent **working +candidate**: its helper, caller, byte semantics, and independent contract checks +have passed isolated Lean checks, and its Rust fixtures have passed focused +compiler tests. At the report handoff, its final integrated golden/live check and +publication were pending. Subsequent commits and CI results establish their own +status; these isolated checks should not be read as a completed CI result. + +We distinguish four kinds of evidence: + +- **Observed failure:** a preserved invocation failed at the named stage. +- **Source finding:** the pinned implementation explicitly omits or rejects an + operation. Consequences for stronger safety claims are deductions from that + source, not necessarily executed counterexamples. +- **Integration restriction:** our checker deliberately accepts less than the + upstream tools to avoid claiming semantics we have not supplied. +- **Historical result:** an older pin exposed a problem; that is not a claim + that the October pin still has it. + +The [lowering audit](LOWERING_AUDIT.md) enumerates the pinned statement/rvalue +languages and relevant transformations. It is not a proof of every translator +pass. This report is an inventory of encountered limitations and identified +semantic gaps, not a claim to have enumerated every possible translator bug. + +## What we are trying to verify + +Our initial proofs concern padding, rounding, layout composition, DST sizing, +cast planning, integer/byte computations, and the numerical parts of allocation +and split operations. We use independent recursive Rust-layout semantics and +explicit premises connecting those semantics to Rust's documented behavior. +Compiler assertions and regression tests challenge those premises; they do not +formally verify rustc. + +More recent work attaches laws to actual unsafe-trait implementation dictionaries +and consumes those laws in generic functions. Examples include `Unaligned`, +`IntoBytes`, `FromBytes`, and `FromZeros::new_zeroed`. The next candidate proves +a generic owned conversion using `ManuallyDrop` and standard `transmute_copy`. + +These are conditional claims. A function's admitted inputs and requirements must +hold, its execution must satisfy the chosen total or partial correctness rule, +and successful outputs must pass their mathematical decoder. This does not yet +establish Anneal's stronger whole-program promise that every caller satisfies +all safety obligations, including resource and temporal obligations. + +## Reading map + +| Area | Main obstacles | Present disposition | +| --- | --- | --- | +| Trait extraction | Residual associated equalities, recursive dictionaries, mixed declaration groups | Generic `KnownLayout` remains blocked; a specific `FromBytes` cycle was refactored away | +| Identity and source binding | Tuple flattening, macro origins, erased default-method bounds, semantic providers | Small upstream patch plus substantial downstream audits | +| Representation | Invalid values disappear into typed Lean carriers; bytes, padding and provenance are absent from ordinary values | Explicit physical decoders and guarded primitive models | +| Execution safety | Drop, unwind, place and implicit guards may be omitted | Closed admission with kernel proofs for empty drops; other unsupported execution rejected | +| Control flow | Production macro's exitless helper loop; a never-returning conversion failure | Separate extracting helper; original macro remains unproved | +| Pointer and memory operations | Value-only pointer carrier, unsupported raw-address operations, no resource semantics | Mathematical value foundations; native execution generally rejected | +| Proof ergonomics | Raw/model bridges, dictionary-law plumbing, loop and theorem registration adapters | Reuse upstream WP/tactics; small local interfaces | +| Reproducibility | Error-bearing output, partial artifacts, toolchain pins, cache provenance and host packaging | Strict fresh final CI; faster provisional development separately | + +## 1. Trait and declaration extraction + +### 1.1 Residual associated-type equalities block generic `KnownLayout` + +**Observed; Aeneas and Charon interaction; unresolved for the generic target.** +Charon successfully extracts both of these cases: + +1. A generic caller with an explicit `KnownLayout` bound. +2. A generic caller without that explicit equality, whose `KnownLayout` trait + itself requires + `::PointerMetadata = Self::PointerMetadata`. + +Aeneas rejects them at +`src/symbolic/SymbolicToPureTypes.ml:1000–1001`, which requires the associated-type +constraint list to be empty. The second fixture matters: removing the caller's +equality does not remove the equality required by the trait. + +This is not a blanket lack of associated-type support. Small acyclic equality +fixtures succeed. Charon's Aeneas preset already requests associated-type +lifting. Its lifting pass deliberately avoids expanding a self-referential +associated-type cycle indefinitely, leaving a constraint that Aeneas cannot +translate. Changing the order of command-line options is not a solution. + +A decomposed recursive fixture gets past one equality and then fails on residual +associated types at `SymbolicToPure.ml:224`. Bounded associated declarations and +implied clauses encounter additional restrictions at `:238–243`. The pinned +`parameterize_trait_types` configuration reference is not a working alternative: +its projection path is unimplemented. + +**Effect on zerocopy:** we cannot yet state and prove the complete generic +`KnownLayout` invariant against the faithfully extracted dictionary. In +particular, we cannot silently remove its `MaybeUninit` metadata equality and +claim to have verified the original trait. + +**Current workaround:** prove concrete local associated-constant initializers +and numerical descriptor operations. Our `[u32]` layout harness follows the +actual local initializer, checks its fields and every element count, and rejects +a deliberately wrong initializer. It is not a generic trait proof. + +**Needed upstream support:** retain equalities through signature translation; +either normalize both paths to the same type parameter or provide checked Lean +equality evidence and use it for the required transports. Preserve the original +associated slot, clause/parent path, and final projection/parameter mapping. +Selective lifting of acyclic components may reduce the problem, but the recursive +relation must remain represented. Deleting the assertion or clearing the +constraint is not faithful support. + +Evidence: [capability fixtures and exact outcomes](tests/capabilities/README.md). +The local historical evidence directory +`into-bytes-front-end-20261013/evidence/knownlayout-summary.md` contains seven +minimal probes and the Charon lifting analysis. + +### 1.2 Recursive trait dictionaries and mixed groups have narrower support than recursive functions + +**Observed and source-confirmed.** Aeneas supports recursive functions, some +mutually recursive functions, recursive data types, and a singleton recursive +trait implementation in Lean. The relevant missing cases are recursive trait +**declarations**, mutually recursive trait **implementations**, and mixed groups +of trait dictionaries, functions, closures, and types. + +The restrictions are explicit in `src/Translate.ml:1183–1256`. A finite Rust +trait declaration graph can become a recursive dictionary representation that +cannot simply be emitted as independent Lean records. Full support needs a +finite, well-typed representation of that recursion; not every dictionary cycle +is an ordinary positive inductive type. + +**Historical `FromBytes` blocker:** importing its supertrait method signatures +reached the mutually recursive `Invariants`/`Alignment` group. Even a generic +identity function with `FromBytes` could fail without performing a byte operation. + +**Resolved portion:** we refactored `Alignment::read` to take an explicit +reference/aliasing parameter and a pointer with tuple invariants. The current +signature uses `Ptr`, retains `A: Reference` and +`T: Copy + Read`, and preserves the compiler's trait checks. This removes +that particular declaration cycle without deleting its meaning. `FromBytes` +dictionaries and the verified `FromZeros::new_zeroed` path now extract. + +**Unresolved portion:** full pointer-heavy production targets also produced +mixed SCCs involving `Alignment::read`, projection/conversion helpers, and +closures. Removing the declaration cycle does not prove those bodies or solve +every mixed group. Some older design notes still describe the initial +`FromBytes` obstacle; that description is historical, not the present frontier. + +**Needed upstream support:** group-aware recursive dictionary translation, +including associated types and method dependencies. Start with the small +pointer-free recursive associated-type fixture before the full zerocopy graph. +A requirement to refactor a particular Rust trait cycle may remain a reasonable +interim restriction, but diagnostics should identify that cycle and the +unsupported group kind directly. + +Evidence: [current pointer invariant code](../../zerocopy/src/pointer/invariant.rs), +[zeroed proof](lean/Proofs/Zeroed.lean), and local +`trait-read-tuple-evidence-20261014/README.md` plus `production-targets/`. + +### 1.3 Excluded provided methods still imported unwanted declaration dependencies + +**Observed Charon bug; locally patched.** Traits contain methods irrelevant to +the operation we want to prove. Excluding an unused provided body did not always +prevent its signature or an implementation override from being discovered. +Those signatures could import the very unsupported trait group we intended not +to execute. + +**Workaround:** our Charon patch applies exclusion consistently during trait +signature discovery and implementation discovery. A reached reference to an +excluded method is an error. Required methods remain required; we do not remove +their signatures to make a trait appear simpler. + +**Needed upstream support:** consistent demand-driven discovery across default +methods, their signatures, overrides, dictionary fields, and actual call +resolution. Preserve the distinction between an interface dependency and an +executed body. Broad opacity is not equivalent: one experiment made +`ConvertError` opaque, then prevented a caller from matching it. + +Evidence: [Charon patch](patches/admission-snapshot.patch), provided-method +controls under [tests](tests/). + +### 1.4 Default-method extraction can erase the unused enclosing `Self` dictionary + +**Observed normalization; downstream semantic binding required.** +`FromZeros::new_zeroed` does not computationally inspect its `Self: FromZeros` +dictionary. Charon can remove that unused argument. The Lean computation is +smaller, but the function's correctness still depends on that trait's promise. + +**Workaround:** recover the exact enclosing trait and method from original +compiler ownership, introduce its dictionary and law as specification premises, +and audit that recovery. We do not invent an extra Rust argument or modify the +extracted computation. + +**Needed upstream support:** stable original-to-final binder/clause provenance, +including an explicit record of erased assumptions. A proof interface should +make computational erasure compatible with retaining logical premises. +Recreating bounds from generated names alone is too fragile. + +Evidence: [ZeroedAudit.lean](lean/ZeroedAudit.lean), +[TraitLawsSupport.lean](lean/TraitLawsSupport.lean), and +[the enclosing-bound documentation](README.md#frombytes-fromzeros-and-owned-zero-construction). + +### 1.5 Trait bounds are computational dictionaries, not automatically proved laws + +**Integration requirement, not a missing Rust trait translator.** +Aeneas can lower many traits and dispatch through dictionaries. That does not +supply the semantic assertion that an unsafe trait is meant to promise. For +example, `T: Unaligned` must provide evidence that alignment is one; +`T: FromBytes` must provide the construction law for both language and library +validity. + +Our `TraitLaws.*` propositions are indexed by the **actual** extracted dictionary +and the selected model providers. Generic contracts consume those propositions. +Implementation checks discharge them for actual impl dictionaries without adding +extra assumptions. Nameless `invariant_proof` markers give a reviewer a visible +request; reached unmarked implementations still incur obligations. + +**What upstream support would help:** an optional law layer tied to native +trait/impl identities, with preserved parent and associated-type paths. It could +remain separate from computational records. Automatically assuming every trait's +law without enforcing implementation obligations would merely move a +load-bearing gap into the tool. + +**Remaining local limitations:** our bridge handles a restricted generic grammar. +Associated-type law parameters, higher-ranked executable bounds, richer const +generics, and trait-bound nominal model assembly need additional local support +as well as faithful upstream extraction. Not every such rejection is an Aeneas +limitation. + +### 1.6 Cross-crate constants can become external templates + +**Observed emission boundary.** A standalone fixture depending on zerocopy can +emit a call to `KnownLayout::LAYOUT` while leaving its initializer as an external +axiom template. That is successful translation of an interface, not verification +of the constant's value. + +**Workaround:** put the relevant harness inside zerocopy so extraction follows +the actual local initializer. The concrete slice initializer is now proved. +For deliberately external primitives, supply a reviewed interpretation instead. + +**Needed support:** precise, documented body-availability/opacity controls and +provenance for dependency bodies and constant initializers. A dependency's +precompiled optimized MIR cannot silently substitute for the inspected stage. +Templates should remain visibly incomplete until an interpretation is supplied. + +## 2. Identity, annotation provenance, and generated interfaces + +### 2.1 Tuple/newtype flattening destroys distinctions needed by model providers + +**Observed default policy; resolved by exposing an existing option.** Different +Rust tuple structs can lower to the same tuple or payload type. Our earlier +`RoundingAlignAndPhase(NonZeroUsize)` example therefore did not initially retain +a nominal one-field Lean structure. Typeclass instances and decoders for +otherwise different Rust types could collide. + +**Workaround:** a small CLI patch exposes the existing +`Config.use_tuple_structs` setting. We pass `-use-tuple-structs false`, preserving +nominal constructors and fields. Tests cover constructors, projections, patterns, +updates, generics, and empty tuple structs, and retain an unpatched/default-mode +oracle. + +**Needed upstream support:** expose the switch without changing its default, +and test nominal extraction comprehensively. Reconstructing lost identity by +editing aliases downstream is not a principled substitute. + +### 2.2 Duplicate trait parent field names produce invalid Lean + +**Observed generation bug.** `ZeroablePrimitive` needs `Copy Self` and +`Copy NonZeroInner`; the pinned backend generates the same `markerCopyInst` +field name for both. + +**Workaround:** a narrow structural repair renames the second declaration and +matching initializers to `innerCopyInst`. It verifies the expected output shape +and preserves both dictionaries. It does not delete a parent clause. + +**Needed upstream support:** unique, stable names based on clause identity, with +matching constructor initializers and metadata. A regression should retain two +instances of the same parent trait applied to different types. + +Evidence: [rename_copy_fields](prepare.py). + +### 2.3 Ordinary doc comments do not provide sufficient macro provenance + +**Observed integration obstacle; Charon extension.** Our specifications and +impl markers originate in Rust doc fences. Macro invocation arguments can supply +a marker that is forwarded, duplicated, transformed, or discarded. Surface text +alone cannot determine which expanded impl it decorates. Expanded doc text alone +cannot establish which source fragment it came from. Tuple-struct constructors +can also share synthetic attributes with the type owner. + +**Workaround:** a source lexer/parser discovers reserved annotations; a patched +Charon records a whole-HIR attribute/owner census, literal origins and source +spans before root selection. Exact doc-origin/span selectors independently root +positive impls. The tooling reconciles source fragments with expanded owners in +both directions and rejects missing or ambiguous associations. Constructor +aliases receive a narrow explicit treatment. + +**Needed upstream support:** a supported provenance record for each retained +attribute fragment, its source literal and expansion context, exact native owner, +configuration, and transformed owner. A complete census must include otherwise +unsupported nodes, so an annotation cannot disappear before reporting an error. +Rust attributes should not need to become a second ad hoc parser for executable +Rust. Derive-generated proof markers remain a deferred integration problem, not +proof that ordinary declarative macros are unsupported. + +### 2.4 Native export metadata exists, but does not replace independent binding checks + +**Existing upstream capability with remaining integration needs.** We use +`-emit-json` and `translation.json`; this is not a metadata exporter we invented. +The native tables already identify functions, types, globals, traits and impls, +with ownership, names and relevant effect information. + +They do not by themselves establish the correspondence between original compiler +arguments, transformed arguments, model-provider suffixes, generated source and +compiled Lean declarations. A global's native ID can also differ from the ID of +the function that computes its initializer. Our static size assertion exercises +that distinction. + +**Workaround:** join native IDs with original/final compiler evidence, then inspect +the compiled Lean environment. Enforce closed inventories and exact argument and +provider identities, not just matching names or definitionally equal carrier +types. Track constant initializer edges as well as ordinary calls. + +**Useful additions:** schema/stage identifiers, stable binder/field/clause maps, +explicit erased-origin records, and global-to-initializer identities. Preserve +native metadata as the primary interface; scraping generated Lean text should +remain limited to framing checks the exporter does not supply. + +### 2.5 Generic external models need semantic parameters absent from Rust computations + +**Observed extension requirement.** A generic physical operation such as +`zeroed` needs to know which physical decoder and mathematical admission rule +interpret `T`. A Rust computational dictionary does not supply our Lean +`RustModel T`. + +**Workaround:** `native_models` preserves the original argument prefix and native +function expression, and appends only the semantic providers its elaborated body +needs. Capture propagates through actual dependencies. The compiled audit checks +that forwarded calls use the exact original providers, including when different +Rust meanings share a Lean type. A same-type replacement provider is not accepted +merely because it typechecks. + +**Needed upstream support:** an explicit primitive-interpretation interface with +checked semantic parameters and effect classification, native binder maps, and +well-defined propagation through generic callers. This would replace our small +Lean/Python extension, not require baking zerocopy's particular model into Aeneas. + +## 3. Physical representation and unsafe execution + +### 3.1 Typed values hide invalid representations before a contract can inspect them + +**Fundamental abstraction boundary.** An extracted Lean `Bool` has no value +corresponding to byte `2`; an enum constructor has no invalid stored tag. +Record fields do not retain padding or arbitrary physical discriminants. +A proof that every Lean Boolean is valid says nothing about the Rust operation +that may have produced an invalid Boolean before lowering. + +**Workaround:** validate candidate bytes or integers before constructing the typed +carrier. Guarded interpretations return `.fail .undef` outside the permitted +language domain. Mathematical/library decoding follows separately; it cannot +retroactively detect an operation erased before reaching that domain. + +**Needed upstream support:** a physical-to-typed boundary that retains the source +storage and checks language validity before introducing typed logical values. +It must handle niches, initialization and metadata, not just reinterpret a +well-typed Lean value. Ordinary safe functional lowering can remain unchanged +where its assumptions are justified. + +### 3.2 Copies and moves do not retain physical storage events + +**Pinned source finding; major safety boundary.** Aeneas transfers logical values, +not a persistent byte store. Typed copies may forget padding; writes to padding +cannot automatically be treated as preserved facts after arbitrary transfers. +This affects an exact-storage model of `MaybeUninit`, `assume_init`, unions, +transmutation and byte-level observations even when the function is annotated. + +[Issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405) is the issue we +filed for typed copies. This report relies on our pinned audit and recorded +issue reference; it does not claim a fresh verification of that issue's status. + +**Conservative plan:** forget all padding contents and initializedness from the +outset, including when a write would physically precede any typed copy. This +rejects some valid Rust programs but does not falsely promise preservation. +Writes still evaluate their arguments and must satisfy access obligations. +This plan is not an implemented general runtime storage semantics. + +**Needed support:** retain typed-transfer events, or provide an explicit +abstraction rule that soundly forgets precisely the permitted storage facts. +A richer carrier alone is insufficient if implicit transfers remain invisible. +Keep provenance placement abstract; do not invent a per-byte provenance rule +that Rust has not committed to. + +### 3.3 Pure AM-byte decoders are not a runtime memory model + +**Current local foundation and remaining scope.** The shared `Rust.Storage` library +has initialized numeric bytes, uninitialized bytes, physical decoders, arrays, +metadata-indexed storage decoders, and cast-composition laws. Those are ordinary +pure Lean values. They do not cause Aeneas to expose reads, writes or typed +transfers. + +The physical relation must correspond to actual Rust layout and language-valid +representations. Initialization alone is vacuous for an always-rejecting decoder. +Our candidate strengthens `IntoBytes` with source realizability: each admitted +source value has some represented bytes. This remains vacuous for an +uninhabited source, as required; it does not manufacture a ZST token or establish +an external-state invariant. + +`FromBytes` completeness includes both language decoding and mathematical/library +admission. `FromZeros` requires both stages for all-zero storage. The model +constraints can be proved automatically without proving that a decoder describes +its input as a human intended. We therefore assess models through operation +contracts; we do not impose a universal injective encoder or canonical +representation requirement that would, for example, forbid hidden hash seeds. + +**Needed support:** reusable physical profiles connected to emitted type facts, +with explicit coverage and trusted premises. The meaningful upstream target is +a model interface and validated primitive boundaries, not a theorem that an +arbitrary user-authored decoder must be the uniquely correct abstraction. + +### 3.4 Generic layout facts are not a universal ABI model after type erasure + +**Observed information gap.** Lean `Type` is not a Rust type descriptor. +Different Rust meanings can erase to one carrier. Generic `size_of`, alignment, +DST metadata and associated layout constants therefore need more information +than the bare lowered type supplies. + +**Workaround:** explicit data inputs for ABI reads; independent recursive layout +semantics; metadata-indexed decoders; and compiler assertions for concrete +profiles. Charon already retains compiler-chosen layout values and expressions +for guaranteed facts. We can challenge our Reference-based calculations with +Rust compile-time assertions without first inventing an Aeneas memory model. +Those assertions check the configurations compiled, not every ABI. + +The generic transmute candidate's `sameSize` premise ties both ordinary ABI +queries to both physical widths. We rejected changing existing total `size_of` +semantics to fail for an arbitrary oversized mathematical decoder, because that +would narrow existing contracts. Physical-model correspondence is explicit. + +**Needed support:** preserve stable Rust type/instantiation identities and expose +available layout/metadata observations as data with their provenance and scope. +Keep compiler choices distinct from language guarantees. A layout descriptor +must model inner padding before outer rounding for nested DSTs; outer alignment +alone is insufficient. Layout, bit validity, optional library invariants, +`usize` bounds and `isize` object-size bounds remain distinct facts. + +### 3.5 Raw-pointer signatures can emit without useful pointer semantics + +**Observed emission and pinned backend limitation.** `RawPtr.lean` has a carrier +with `v : T`, not an address/provenance/metadata representation. Its scalar cast +returns `.fail .undef`. Native probes can emit raw-pointer signatures while +leaving slice-pointer construction, `NonNull` and its operations as external +axiom templates. That is not an admitted pointer proof. + +A production `IntoBytes` path separately failed on `&raw const (*self)` and +`&raw mut (*self)`. These are actual extraction rejections, distinct from the +successful signature-only probes. + +**Workaround:** reject general native pointer execution; use narrow reviewed +boundaries for selected byte operations. The shared `Rust.Pointer.Value` model +already describes addresses, opaque optional provenance and metadata, with casts +that preserve provenance. It is a mathematical foundation, not a replacement for +the native carrier or permission to dereference. + +**Needed support in stages:** first a faithful pointer-value carrier and cast/ +metadata operations; then storage/access interpretations with alignment, +initializedness and bit-validity guards; finally permissions, aliasing, allocation +ownership and liveness where those claims require resources. Value-only pointer +reasoning need not wait for a complete resource logic. Do not decide where +provenance lives in pointer bytes beyond documented Rust guarantees. + +### 3.6 References, boxes and allocations lose spatial and resource observations + +**Deliberate upstream functional abstraction.** References become referent values; +`Box` becomes `T`; box construction is eliminated and allocator parameters +can be hidden by the preset. Aeneas's borrow analysis is useful and substantial, +but the pure result does not retain allocation identity, address alignment, +retagging, access permissions, lifetime extent, allocator effects or ownership +resources. + +**Effect:** we can prove interval bounds, disjoint numerical ranges, layout gates +and allocator argument preparation without having proved reference creation, +actual allocation or full pointer validity. The production paths consuming those +facts still require their Rust safety arguments. + +**Needed support:** preserve those observations or expose explicit abstract +operations and premises for the claimed layer. Full resource modeling is a +separate larger project; adding a size theorem cannot supply liveness. + +### 3.7 Residual drops do not execute destructors in the default interpretation + +**Pinned source finding that became an actual prerequisite.** Default `Drop` +interpretation is a no-op. `-eval-drops` invalidates a logical value and processes +loans; it does not execute its arbitrary destructor body. Charon's +`--precise-drops` adds `Destruct` bounds and requires at least elaborated MIR, +which is a different inspection stage. Neither flag is a one-line repair for +our promoted-MIR admission theorem. + +The real generic transmute helper retains conditional drops on moved argument +and temporary slots, including normal and unwind paths. Rejecting all drops +would reject this useful program; accepting them without an argument could hide +a destructor with arbitrary unsafe effects. + +**Implemented workaround:** a conservative ownership analysis over the complete +compiler body. Lean proves accepted whole-local conditional drops empty, and +therefore unable to execute destructor glue. Fresh certificates are bound to the +exact body, snapshot, native identity and checker source. Uncertain joins, +projections, partial moves, cycles and meaningful drops fail closed. Unreachable +and unwind blocks are not silently omitted from the structural audit. + +**Needed support:** accurate initialization/drop-flag semantics and explicit +execution of destructor glue, including generic and unwind destruction, or an +upstream-supported certificate that an erased drop cannot execute. Preserve the +inspection stage and its meaning. A proof that an empty slot has no destructor +effect does not prove arbitrary destructors harmless. + +Evidence: [DropOwnership.lean](lean/DropOwnership.lean), +[DropJson.lean](lean/DropJson.lean), [DropAudit.lean](lean/DropAudit.lean), and +[drop_ownership.py](drop_ownership.py). + +### 3.8 Panic, UB and unwind termination are not preserved uniformly + +**Pinned source finding.** Charon distinguishes these abort kinds. Aeneas maps +all `Abort` forms to a symbolic panic node, ignores the failure kind on `Assert`, +and ignores `on_unwind` blocks during call/assert interpretation. + +**Workaround:** total and partial contracts both reject failures. Reviewed unsafe +primitives use the existing `.fail .undef` marker, and sequencing preserves it. +Even `ensures _ => True` cannot accept that result. We audit original cleanup +execution and reject unsupported effects before they are erased. + +This is not a new Result constructor patched upstream: `Error.undef` already +exists. It means no permitted execution claim here and is also used by backend +unsupported models; it is not always a diagnosis that actual Rust has UB. + +**Needed support:** preserve failure kinds and cleanup effects, and distinguish +fatal forbidden execution from recoverable panic in any future handlers. A +thread-spawn model that returns successfully while hiding a child's UB would +break the intended safety claim even if it correctly ignores child termination. +We do not yet model thread spawn, panic catching or panic-tolerant contracts. + +### 3.9 A convenient failure-erasing adapter is unsafe to reuse indiscriminately + +**Existing API with a restricted applicability.** `Option.ofResult` can turn every +failure, including `.undef`, into an ordinary `None`. That can be appropriate +inside a reviewed checked-arithmetic model, but is not a faithful implementation +of arbitrary Rust recovery from forbidden execution. + +**Workaround:** follow compiled downstream dependencies, including opaque helpers, +and reject uses of this adapter in admitted executions. Stop at explicitly +reviewed backend primitives, whose implementation has its own trusted contract. +Independently audit complete external definitions: blacklisting one adapter alone +cannot rule out a hand-written failure-erasing match. + +**Needed support:** effect-specific recovery interfaces or a result/effect design +in which UB cannot be accidentally handled as panic. Retaining the distinction +through interpretation and handlers matters more than adding a tag. + +### 3.10 Place mentions and CPU-feature obligations can be absent from the pure body + +**Pinned source findings.** Charon notes that invalid projections in +`PlaceMention` can cause UB; Aeneas treats it as a no-op. Aeneas also has a pass +for inserting `target_feature` assertions, but its flag is off by default and +our driver does not enable it. + +**Workaround:** inspect the original dependency closure, validate or reject +projection shapes and unsupported attributes, and keep these premises visible. +A supported operation must supply its implicit access/CPU conditions. + +**Needed support:** checked place evaluation and explicit feature premises or +admission. Enabling a feature-gate pass solves only that particular obligation; +it does not justify erased storage, destructor or pointer effects. + +### 3.11 Builtin replacement and infallibility classification affect what survives + +**Trust boundary, not just template filling.** A builtin can replace a visible +Rust body, so auditing that unused body does not audit the executed Lean model. +An operation classified as pure and infallible can also lose unused calls or +repeated evaluations before a downstream safety guard is added. + +**Workaround:** select and audit the actual interpretation, exact Rust endpoint +pairs, generated failure-capable signature, complete compiled definition and +call bindings. Preserve argument evaluation and failure even when a result is +ignored. Local opaque helpers have exact body hashes; external standard-library +operations have explicitly reviewed semantics. + +**Needed support:** a first-class interpretation registry with effect and +correspondence information, validated against the original signature and use. +A user-supplied unsafe model must not be allowed to add failure after the +translator has already treated the operation as infallible. + +### 3.12 Deterministic results do not automatically cover representation ambiguity + +**Real design pressure; current bounded downstream solution.** Aeneas's current +`Result` is an interaction tree whose Rust effect interface contains failure, +not arbitrary storage-read choices. A fixed raw value can admit multiple byte +representations, and converting it to a byte-observing destination can expose +those differences. Proving only a chosen canonical output would lose behaviors. + +**Candidate workaround:** a checked representation preference in each retained +model provider, a generic proof quantified over that provider, and a coverage +theorem varying only the preference while fixing the decoders. Tests produce two +different destination values from the same raw source. No injective encoding or +single canonical representation is imposed. + +This preference is a function of the raw value, not execution history. Admission +therefore restricts the first fragment to one conversion per execution and +polymorphic forwarding that keeps the provider universally bound. Repeated +calls, loops, recursion or concrete forwarding can correlate or fix choices and +are rejected. These are **our restrictions**, not Aeneas's general loop or +recursion limitations. + +**Needed support:** explicit state or a suitable nondeterministic effect with a +universal/demonic WP, or another abstraction with a proved coverage theorem. +Thread choices through extraction and optimizations. A general interaction-tree +library is useful infrastructure, but the concrete Rust effect interface and +extracted computations must actually expose the effects in question. + +## 4. Earlier compiler transformations and complete admission + +### 4.1 The requested MIR stage is not enough unless the actual body origin is checked + +**Source-confirmed hazard; Charon patch.** Promoted MIR can be unavailable because +rustc has stolen a body, and upstream can fall back to optimized MIR. Aeneas +cannot reconstruct an already-erased unsafe event from final LLBC. + +**Workaround:** preserve the imported unstructured body before Charon passes; +reject local optimized-MIR fallback during admission; inspect both that snapshot +and final LLBC; bind exact source/configuration/runtime identities to the result. +Final CI rechecks the evidence rather than trusting a stale report. + +**Needed support:** supported stage-specific snapshots, actual stage/fallback +metadata, body origin and transformation provenance. Final `--ullbc` output need +not mean pretransformation input. + +### 4.2 Optimization level zero does not provide a semantic preservation theorem + +**Important negative result from the design investigation.** Charon already sets +MIR optimization level zero, `mir_preserve_ub`, and `always_encode_mir` for crates +compiled through its wrapper. Thus seeing an `optimized_mir` query is not proof +that optional optimizations ran. Conversely, level zero does not reverse earlier +mandatory lowering, reconstruct source effects, or establish the build origin +of precompiled dependencies and the sysroot. + +**Workaround:** controlled inputs and stage checks, closed original dependency +inspection, and external interpretations for bodies whose relevant origin is +not available. + +**Needed support:** auditable compiler-body provenance and a preservation argument +for the admitted language/effects. Enumerating each observed erasure is useful +but cannot substitute for a compositional account of which observations each +pass preserves. + +### 4.3 Compiler alignment and null checks are deliberately disabled + +**Pinned driver finding.** Charon disables `CheckAlignment` and `CheckNull` +insertion. This avoids compiler-generated checks interfering with its symbolic +model; it also means a missing assertion is not evidence that the corresponding +Rust access has no alignment or non-nullness requirement. + +**Workaround:** reject unsupported memory operations, or add explicit semantic +guards to their reviewed interpretations. A pointer-valued cast need not require +dereference permission, while a read or reference creation does. + +**Needed support:** expose operation preconditions directly, rather than relying +on incidental rustc debug checks. Enabling those checks alone would still not +model initialization, allocation bounds, provenance or aliasing. + +### 4.4 Process success and generated files do not certify a complete translation + +**Observed tool contract hazard.** Historical Charon runs exited zero while +emitting `has_errors: true`, missing/partial declarations and warnings. Upstream +failures can also leave files behind. A file's existence or a successful wrapper +command cannot certify extraction. + +**Workaround:** strict flags; require the explicit success marker; verify closed +owner/dependency inventories; reject unknown shapes, errors, missing declarations +and unapproved axioms; stage outputs; and compare fresh goldens and live proofs +independently. The local checker validates the complete relevant schema rather +than guessing unfamiliar constructors or serialization references. + +**Needed support:** an unambiguous complete-success contract, structured stage +errors, atomic publication of successful output, and explicit schema/version +metadata. External axiom templates should not resemble completed proofs. + +## 5. Specific control-flow and backend failures + +### 5.1 An exitless loop in the production `transmute!` helper is rejected + +**Observed.** The macro's compile-time trait-check helper retains an infinite loop +without a `break`. Aeneas rejects it at `InterpLoops.ml:411`. Direct calls to the +standard transmute primitive extract, isolating the macro-helper issue. + +**Workaround:** first prove direct concrete standard transmutations. The current +candidate adds a real trait-bounded const `transmute_copy` helper and a generic +caller with the size assertion in the executable helper. The production macro +is unchanged and has not acquired a proof merely because the helper works. + +**Needed support:** translate no-exit loops into an appropriate divergent +computation **while retaining their body effects**. Replacing every syntactically +infinite loop by `.div` would hide a panic, unsafe operation or state effect that +occurs first. Better reachability/declaration selection may avoid importing a +nonexecuted type-check helper, but must retain the compiler-checked trait facts. + +### 5.2 A never-returning error conversion produced an internal failure + +**Observed historical production probe on the current pin.** +`From> for !::from` / `alignment_impossible` failed with +`Unexpected result: Cps.Unit` in `interp/Interp.ml:593`. + +No verified general repair has been recorded. This is a separate control-flow +frontier from the generic trait-cycle failure and from resource semantics. +An upstream regression should retain the exact never-returning conversion and +its call context. A suitable `Result Empty`/divergence interpretation must not +turn a forbidden operation before non-return into an acceptable divergence. + +Evidence: local `existing-unsafe-path-probe-20261013/aeneas.log`. + +### 5.3 Mutable suffix reconstruction is incorrect in a pinned slice builtin + +**Observed backend model bug; avoided.** +`SliceIndexRangeFromUsizeSlice.get_mut` reconstructs an updated slice using a +modified suffix followed by the old suffix, rather than the original prefix +followed by the modified suffix. + +**Effect:** a proof about an offset write could describe the wrong updated +sequence even though the Rust operation and Lean types look reasonable. + +**Workaround:** leave the builtin unregistered; use a narrow local offset-copy +boundary with exact prefix/copy/suffix semantics and full body/signature checks. + +**Needed upstream repair:** correct reconstruction, and prove length, unchanged +prefix, replaced region and unchanged suffix laws. Exercise boundary offsets, +empty replacements and nonempty prefixes. This is a correctness defect, not +merely a request for a more convenient lemma. + +### 5.4 Some borrow and type forms remain outside the relevant fragment + +**Mixed evidence; do not overgeneralize.** Aeneas supports substantial borrow +functionalization, returned references, closures and recursive functions. Our +current admission checker deliberately rejects escaping borrows, arbitrary +callbacks, function-pointer calls and unreviewed dynamic dispatch. + +A returned mutable borrow can expose a backward reconstruction function rather +than an ordinary updated value. Automatically checking only the visible return +would miss validity of the state reconstructed later. We currently reject that +specification shape instead of implying the hidden state was validated. + +Pinned source also has restrictions on ADTs with nested mutable borrows, +unsupported function-arrow/dynamic trait shapes, generic associated types and +bound/implied-clause shapes. The historical research includes nested-borrow +failures on older pins; they are not evidence of a current flaky reproducer. + +**Needed work:** distinguish a source construct that cannot extract from a +functionalization our contract assembler cannot yet express. For supported +backward functions, expose the argument/result/state relation and attach +higher-order validity contracts. For actual unsupported shapes, retain minimal +regressions and improve diagnostics rather than treating all references or +closures as unsupported. + +## 6. Proof and model ergonomics: what was already available + +These items caused development cost, but much of the needed foundation already +exists upstream. Reimplementing it would increase the maintenance burden. + +### 6.1 Total and partial correctness already have the needed basic meanings + +`WP.spec` requires successful termination. `WP.dspec` can permit divergence. +Both reject failure; partial correctness is not permission for panic or UB. +Our concise `spec` language builds on these predicates, automatically checks +input/output decoding, and requires an execution judgment even for a trivial +postcondition. We tested panic and divergence explicitly. + +The syntax, raw/mathematical scopes, decoder completion and required-contract +checks are downstream interfaces. They are not evidence that Aeneas lacked +contracts. Upstream `spec_mono`/`dspec_mono` already support mathematical-view +adaptation. Our original contract migration became verbose in part because it +also strengthened propositions; that was not fundamental to macro syntax. + +### 6.2 Checked arithmetic and indexed loop proofs mostly needed reuse and adapters + +Aeneas already supplies exact checked-add/subtract/multiply rules, `step_pure`, +scalar tactics, well-founded `loop.spec` and `loop.spec_decr_nat`. We reuse them. +Our indexed-loop adapter packages a natural measure, a prefix model and the +specific invariant shape useful for byte/layout computations. The body must +still prove progress, bounds and prefix preservation. + +Rust finite-word operations and `Nat`/`Int` views create bridge goals. General +rounding, powers of two, bitwise encodings, overflow outcomes and nested layout +algebra still need domain lemmas. This is largely library/automation work, +not a request for a second arithmetic or termination semantics. + +**Useful improvements:** better maintained bridge lemmas and simp sets, stronger +standard primitive specs where appropriate, reusable loop-shape adapters, and +local diagnostics that identify the missing arithmetic fact. Preserve APIs whose +`Option` result intentionally describes overflow on all inputs. + +### 6.3 Callee theorem reuse needed declaration assembly, not a new proof calculus + +Ordinary Lean imports, named theorems and Aeneas's `[step]` registry suffice for +many caller/callee proofs. Our spec wrapper initially required a small registration +adapter because the registry inspects theorem types syntactically. Explicitly +expanding just the specification alias makes the existing registry usable. + +**Useful improvements:** robust registration through transparent proposition +wrappers and structured declaration dependency feedback. Avoid requiring proof +order to follow source-comment order. Associated compiler/native identities and +real import dependencies are more reliable than a second custom proof graph. + +### 6.4 Automatic model derivation has deliberate local limits + +Our recursive *field composition* supports structural products, arrays, options +and selected wrappers, but our automatic *nominal declaration* derivation rejects +recursive/indexed groups and several richer generic shapes. These are not the +same restriction, and recursive Lean data extraction upstream does not imply +our decoders can be derived automatically for every such type. + +Proof fields in mathematical model structures often follow from routine bounds. +We added decoder-scoped completion using ordinary tactics rather than imposing +a separate model-level proof language. Raw-to-mathematical bridges remain a +reusable-lemma opportunity. No extra upstream syntax is necessary for this +completion; Lean's elaborator/tactics already provide the mechanism. + +### 6.5 Source meaning and editor support required local tooling + +A proof can establish a proposition weaker than a reviewer intended. Our +independent required-contract families compare the authored contract against an +expectation for an arbitrary execution outcome before specializing to the actual +function. They are semantic sanity checks, not extra axioms or a replacement for +the Lean kernel. Reviewers still need to look for vacuous preconditions, early +returns and observations that discard the intended property. + +Editing generated Lean gives native editor support but copying comments back was +awkward. Deterministic projections, source maps and guarded copy-back now support +that workflow. We track useful generated review snapshots separately from +unfinished editing state. These are integration affordances; they do not require +changing Aeneas's theory. + +**Useful upstream interfaces:** stable names and source maps, native declaration +ranges and semantic metadata sufficient for robust tools. Do not confuse an +editor cache or projection with the authoritative proof source. + +## 7. Reproducibility, deployment and historical tooling issues + +### 7.1 Lean/Aeneas/Charon/Rust versions must move as a compatible set + +Anneal v1 and zerocopy initially used different pins, which prevented a simple +shared-library code move. We updated Anneal, validated extraction fixtures and +bundles, and made Anneal's lockfile the source of truth. The shared `anneal/lean` +package separates pure Rust mathematics from Aeneas-dependent adapters; both +consumers use the same source. + +The historical v1 wrapper also repairs a bare `@[discriminant]` annotation to +`@[discriminant isize]` and marks axiom-calling extracted functions noncomputable. +Those are recorded compatibility accommodations, not freshly reproduced defects +of every current zerocopy extraction. + +**Needed support:** compatible, reproducible releases of the complete graph and +clear compatibility information. Keep consumer-specific extraction options and +patch identity explicit rather than silently forking pins. + +### 7.2 Intel Mac distribution and native library bundling required extra work + +The selected upstream release lacks an `x86_64-darwin` Aeneas archive, requiring a +source-build fallback. Charon's upstream nixpkgs dropped Intel Mac support, so +our packaging follows a compatible locked nixpkgs. Darwin library bundling and +signing needed adjustments for flags unsupported by the available signing tool. +A temporary installer path also needed replacing when Intel support disappeared. + +These are deployment problems, not evidence that the proof semantics differ on +Intel. Native host validation checks the actual portable archive, relocation, +executables and Lean imports. Building OCaml/Rust/Lean dependencies from source +made Intel validation much slower than using supplied binaries. + +**Useful improvements:** reproducible native archives for supported hosts, tested +relocation/read-only installation, complete dependency closure, and explicit +host retirement policy. Our bundle distribution reuses Anneal's existing +exocrate archive mechanism; no new global package manager was introduced. + +### 7.3 Cached builds can validate a different source snapshot + +We encountered stale-import acceptance while using Lake `--old`; changing source +could leave a previously compiled proposition in the environment. A proof audit +can faithfully inspect that stale environment and still miss the source change. +This is a cache/provenance failure, not a contradiction accepted by Lean's kernel +for the newly edited source. + +**Workaround:** rebuild authored roots/shared sources and run source-mutation +controls. Final CI verifies exact source copies, extraction/configuration +identity, both golden/live builds and all discovered annotations. Development +may use incremental cached extraction, but labels its result provisional and +cannot substitute it for final verification. + +**Useful improvements:** straightforward hermetic build entry points and +verifiable source-to-artifact identities. Faster development should avoid +unnecessary extraction without weakening the final path. Repeated fresh +admission/kernel checks are real integration cost; optimize through a justified +cache boundary, not by trusting stale reports. + +### 7.4 Diagnostics and error provenance materially affect development time + +Internal assertions, generic `Unsupported` errors and large mutually recursive +group dumps often identify an implementation location without explaining the +Rust dependency that imported it. Generated names and wrapper propositions can +also make tactic failures harder to relate to Rust. + +Our workaround is small permanent native capability fixtures, preserved raw +errors and source snapshots, mapped Lean diagnostics, compiled inspection, +negative controls and exact pin records. A failing check must fail for the +intended reason; a new syntax error is not evidence that a safety audit works. + +**Useful improvements:** structured errors naming original item, construct, +originating dependency edge, unsupported stage and available alternative; robust +minimal reproducers; and transactional output publication. Keep unsupported +cases as clear errors rather than generated holes that resemble success. + +## 8. Historical findings and investigated capabilities + +The reference research is broader than the current zerocopy implementation. We +mechanically searched all 658 `reports/*/REPORT.md` documents on its local branch; +416 mention Aeneas. We then reviewed the selected headings and passages for +additional limitation classes. That search improves coverage, but it does not +independently reproduce every historical assertion. In particular, none of these +reference documents names our October Aeneas pin. The following findings must +retain their original dates and evidence classifications. + +Report names below are paths under that branch's `reports/` directory. Each +ends in `/REPORT.md`. The evidence section gives the repository and exact branch +checkpoint, so another researcher can read the original reports and artifacts. + +### 8.1 Failed or concurrent generation can leave misleading artifacts + +**Observed on older pins, September 29.** A nonzero Aeneas invocation wrote +partial Lean output containing `sorry`. Some partial output could compile with +`sorryAx`. Reusing an output directory after removing a trait or changing output +mode also retained old external templates. Distinct simultaneous requests could +leave artifacts from different requests in one destination. + +A Charon 0.1.210 concurrency experiment found malformed JSON even when both +writers returned success: one of six direct collision rounds and one of three +Cargo collision rounds witnessed this. These counts are witnesses, not estimated +failure rates. Different files from `--format all` could also disagree about +completeness. + +**Effect:** neither a successful Lean compilation, an existing file, nor the +status of one writer establishes that the complete intended program was +translated. Old declarations can outlive the source that justified them. + +**Current defense:** private destinations, checked process status and completeness, +fresh final generation, source/dependency binding, and transitive axiom audits. +A legitimate external primitive is explicitly modeled; `sorryAx` is rejected. + +**Useful upstream changes:** transactional publication after complete success, +explicit ownership of a destination, generation identifiers in all outputs, +structured success receipts and cleanup rules. A consumer should still avoid +sharing a destination across writers. + +Evidence: `anneal-3730-aeneas-trait-output-shrink-matrix-2026-09-29`, +`anneal-3730-charon-aeneas-boundary-2026-09-29`, +`anneal-3730-aeneas-identity-manifest-2026-09-29`, +`anneal-3730-aeneas-process-contract-2026-09-29`, and +`anneal-3730-charon-concurrency-interruption-2026-09-29`. + +### 8.2 A warm Cargo target can retain another source tree's generated input + +**Observed on an older toolchain, September 29.** A copied source tree reused +another tree's Cargo target. Extraction saw the copied tree's edited function, +but also the original tree's path-dependent generated constant, `205`. A private +target for the copied tree yielded `217`. Both outputs reported +`has_errors: false`. + +**Effect:** an error-free compiler extraction can combine subjects unintentionally +when build-script inputs and output provenance are not isolated. This is a build +identity failure, not evidence of an incorrect arithmetic translator. + +**Defense and needed support:** isolate or rebuild when build origin changes; +record generated sources, build environment and compiler inputs as part of the +subject. Better upstream extraction receipts should identify those inputs. +Hashing only handwritten Rust or checking `has_errors` cannot detect this case. + +Evidence: `anneal-3730-charon-warm-target-controls-2026-09-29`. + +### 8.3 Optional termination generation and effect analysis had separate limitations + +**Historical source findings, June 3; not reproduced on the October pin.** The +optional extrinsic termination mode emitted `termination_by`, `decreasing_by` +and `partial_fixpoint` in a combination incompatible with the inspected Lean +4.30.0-rc2 grammar. Lean decreases mode explicitly rejected mutual recursion, +and Lean fuel mode was unavailable. + +A separate analysis treated trait-method calls as potentially failing but not +diverging or stateful. Such an analysis flag is not a theorem that every Rust +implementation terminates. These findings are distinct from the observed +exitless-loop rejection and from the backend's ability to denote divergence. + +**Our use:** ordinary partial-fixpoint extraction with proof-time total/partial +WP and explicit termination measures. We do not use a native `can_diverge` flag +as proof of successful execution. + +**Needed work:** regression-test optional termination output against its exact +Lean pin; give effect summaries an explicit meaning and conservative treatment +of unknown implementations. State, divergence and failure summaries must agree +with whatever effects callers are allowed to observe. + +Evidence: `aeneas-extrinsic-termination-nightly-2026-06-03`, +`aeneas-infinite-diverging-execution-nightly-2026-06-03`, and +`aeneas-semantic-omissions-unsafe-rust-nightly-2026-06-03`. + +### 8.4 The public libraries do not provide a request-safe incremental service + +**Historical source investigation.** Aeneas's translation pipeline used mutable +process-global configuration and error state, recomputed whole-crate contexts, +and exposed no supported request/reset/cancellation/invalidation protocol. +Charon's compiler extraction driver lived in its binary rather than the public +`charon_lib` interface. + +**Effect:** keeping one process alive does not automatically make extraction +incremental, isolated or safe to run concurrently. An interrupted request may +also have published partial artifacts. This matters to editor integrations and +our attempts to shorten the development loop. + +**Current approach:** ordinary isolated processes; cache only at explicit input +boundaries; offer provisional local proof iteration separately from final CI. + +**Needed support:** explicit session state and dependencies, cancellation and +publication semantics, and a reusable driver interface. An incremental daemon +would be useful only if it preserves subject identity and complete invalidation; +it is not needed for batch verification. + +Evidence: `aeneas-library-process-architecture-nightly-2026-06-03`, +`aeneas-incremental-translation-feasibility-nightly-2026-06-03`, and +`charon-library-process-server-0-1-210`. + +### 8.5 Alias, source-coordinate and safety metadata are not all retained + +**Historical source findings and preserved coordinate observations.** Ordinary +Rust type aliases can disappear as independent declarations; generated comments +contain synthesized names and spans rather than the original prose. These are +source-identity limitations, separate from value semantics and nominal structs. + +Charon serialized display-width columns, but `Loc::to_byte` added a column to a +byte offset. Wide, combining and other Unicode characters distinguish those +units. A plausible-looking source span is therefore not enough for byte-exact +annotation binding. Our newer physical annotation-origin records use byte +offsets; they do not retroactively change the meaning of the older span API. + +The older semantic AST also omitted structural unsafe blocks, unsafe trait/impl +qualifiers and the distinction between static and mutable-static declarations; +function `is_unsafe` survived. Some Rust predicates were omitted, including +`ConstEvaluatable`, `WellFormed`, `HostEffect` and `ConstArgHasType`. The full Rust +well-formedness and authorization context cannot be reconstructed from the +remaining generic-clause list alone. Higher-ranked/lifetime precision also had +known restrictions. + +**Effect:** source annotation coverage, safety review, constant-evaluation +premises and theorem binding require evidence from the stage that still has the +relevant fact. This does not mean every erased qualifier changes the functional +return value. + +**Needed support:** explicitly typed span units, original byte ranges and owner +identities; retained safety/declaration facts; and a documented account of erased +predicates and their compiler-checked evidence. Ordinary aliases need source +correspondence, not necessarily distinct nominal Lean types. + +Evidence: `aeneas-type-alias-handling-nightly-2026-06-03`, +`aeneas-rust-comment-preservation-nightly-2026-06-03`, +`end-to-end-source-correspondence-nightly-2026-06-03-v4-30-0-rc2`, +`cross-tool-utf8-span-columns-2026-09-27`, +`anneal-3731-i079-unicode-charon-spans-2026-09-30`, +`anneal-3731-i079-generated-file-charon-spans-2026-09-30`, +`charon-raw-pointers-unsafe-operations-0-1-210`, and +`charon-traits-generics-nightly-2026-06-03`. + +### 8.6 Pointer casts, foreign interfaces and assembly lose distinctions needed by richer models + +**Historical source findings; not executed zerocopy regressions on our pin.** +Several pointer cast/coercion and exposed-provenance operations became a common +`CastKind::RawPtr(src, dst)` form. That loss of the original operation's meaning +is separate from the later Lean pointer carrier lacking address and provenance. +A strict-provenance interpretation needs both pieces. + +The inspected foreign-function representation omitted `c_variadic` and effective +link-name/ordinal information. Inline assembly omitted operands, register +constraints and options; global assembly was skipped. An external function body +or instruction-set model cannot reconstruct an interface promise already erased. + +**Current policy:** these operations are outside our admitted execution fragment. +No general FFI, assembly or provenance claim follows from the byte mathematics. + +**Needed support:** retain original cast reason and relevant foreign/assembly +interfaces, or reject them before erasure. Then supply explicit guarded semantic +boundaries. Merely accepting more final LLBC constructors would be insufficient. + +Evidence: `charon-raw-pointers-unsafe-operations-0-1-210`, +`rust-extern-foreign-items-nightly-2026-05-31`, and +`rust-inline-global-assembly-nightly-2026-05-31`. + +### 8.7 Existing resource-model research is not yet a source translation bridge + +**Historical capability review, September 26–27.** The observed separation-logic +prototype, at upstream PR #1352 head `75fb1479…`, supplied typed-slot sequential +heap mathematics and proof interfaces. The reviewed source interpreter still +rejected raw-pointer dereferences. The work did not establish byte storage, +provenance, padding, partial initialization or concurrency semantics for our +extracted Rust. + +**Implication:** we should reuse useful libraries, but importing a separation- +logic library or upgrading to a prototype does not itself prove that production +pointer operations have entered that model faithfully. The missing bridge needs +its own supported source fragment, primitive rules and preservation argument. + +Evidence: `aeneas-separation-logic-status-2026-09-26` and +`iris-concepts-for-rust-aeneas-separation-logic-2026-09-27`. + +Other surveyed historical research covered async/coroutines, experimental generic +const/effect/transmutability features and smart-pointer unsizing. We did not +establish that these blocked our current targets, so they are not presented as +encountered zerocopy regressions. Likewise, an old bound-lifetime resolution issue +was already closed before the June review. Anneal v1's safe-mutation/invariant +closure limitations belong to Anneal's policy and frontend; they are not Aeneas +translator defects. Our conditional contracts deliberately make a weaker claim. + +## 9. Recommended upstream work, in order of near-term value + +1. **Remove small, confirmed obstacles.** Expose nominal tuple extraction; + fix duplicate parent-field naming and suffix reconstruction; make provided- + method exclusion consistent; support explicit pretransformation snapshots, + exact body-origin reporting and annotation provenance. Each has a narrow + regression target and removes downstream repair or audit plumbing. +2. **Unblock faithful trait interfaces.** Translate residual associated equalities + with evidence/transports, then handle the required recursive dictionary + groups. Use the pointer-free recursive equality fixture before generic + `KnownLayout`, and retain all Rust constraints throughout. +3. **Make primitive extension and execution admission explicit interfaces.** Bind + original endpoints, semantic providers, effect classifications and native + arguments. Preserve fatal forbidden execution, cleanup and implicit guards. + Emit the information downstream tools currently reconstruct. +4. **Support the next control-flow cases.** Translate exitless loops without + erasing their effects, and fix the never-returning conversion regression. + These unlock real production paths before a full resource model exists. +5. **Add faithful pointer values and physical transfer semantics.** Separate + address/provenance/metadata manipulation from memory permissions. Retain or + conservatively abstract typed transfer, padding and initialization events. + Numeric byte proofs and layout calculations can then connect to more actual + pointer operations without overpromising liveness or provenance placement. +6. **Extend effects/resources only as demanded by the claim.** Independent byte + choices, recoverable panic, concurrency, destruction and temporal ownership + need compositional semantics. The existing interaction-tree and WP libraries + provide infrastructure, but those Rust effects must enter the model and + survive translation before proofs can discharge them. + +The desired end state is not that Aeneas must infer every Rust safety argument. +It is that a downstream proof can state the intended abstraction and explicit +premises, and the extraction either preserves the observations needed for that +claim or rejects the program with a useful explanation. Much of our current +scaffolding exists to enforce that boundary externally. + +## 10. Evidence and reproduction pointers + +The strongest tracked entry points are: + +- [LOWERING_AUDIT.md](LOWERING_AUDIT.md): constructor/handler audit and versioned + representation premises; includes upstream source coordinates and links. +- [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md): admitted operations, rejected effects, + original/final inspection and required failure controls. +- [tests/capabilities/README.md](tests/capabilities/README.md): exact native + `KnownLayout`, macro, primitive and pointer fixture outcomes and replay commands. +- [patches](patches/): the complete local upstream patches. +- [prepare.py](prepare.py), [NativeModels.lean](lean/NativeModels.lean), + [Check.lean](lean/Check.lean), [ZeroedAudit.lean](lean/ZeroedAudit.lean), and + [NativeProviderAudit.lean](lean/NativeProviderAudit.lean): naming repair, + semantic suffixes, compiled and dependency audits. +- [RustRealizability.lean](lean/RustRealizability.lean), + [TransmuteModel.lean](lean/TransmuteModel.lean), and + [Proofs/GenericTransmute.lean](lean/Proofs/GenericTransmute.lean): current candidate + byte bridge, ambiguity coverage and actual generic native proofs. + +Historical evidence is preserved locally under the workspace's `.aeneas-work/` +container. Relevant directories include `erasure-audit-20261008`, +`trait-bound-capability-20261013`, `into-bytes-front-end-20261013/evidence`, +`existing-unsafe-path-probe-20261013`, `trait-read-tuple-evidence-20261014`, +`knownlayout-native-20261014`, `transmute-copy-state-20261015`, +`shared-pin-remote-validation-20261007`, and `shared-pin-bundle-evidence-20261007`. +These are historical evidence pointers, not repository-relative replay dependencies +or caches that CI must consume. Current fixtures and pinned commands are the +preferred starting point for a new reproducer. + +The local `codex/anneal-sdk-reference-reports` branch retains earlier research in +`reports/*/REPORT.md`. Its reviewed checkpoint is +`a0ff759e7d2d9a953f0ac40b326dd23197bd9188`, in the migration's shared Git store +at `/Users/codex/Codex/Migrated/zerocopy/.git`. For example: + +```bash +git --git-dir=/Users/codex/Codex/Migrated/zerocopy/.git show \ + a0ff759e7d2d9a953f0ac40b326dd23197bd9188:reports/anneal-3730-aeneas-trait-output-shrink-matrix-2026-09-29/REPORT.md +``` + +Those reports use several older pins and include successful capability tests as +well as failures. Their date, exact version and preserved stderr matter; a +historical failure must not silently become a claim about the current runtime. + +For upstream source inspection, use the pinned +[Aeneas source tree](https://github.com/AeneasVerif/aeneas/tree/ca282ec2312a96f6a985a4d23a663690816d3f3e) +and [Charon source tree](https://github.com/AeneasVerif/charon/tree/cf02e3f228f97ee7be3a415be56989053063326d). +Source coordinates in this report refer to those trees unless explicitly marked +historical. Existing upstream facilities are often part of the solution; this +report should not be read as a proposal to reimplement their WP, borrow analysis, +trait dictionary extraction, arithmetic tactics or native metadata exporter. diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 91f3ef3550..5b7c823e7f 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -13,6 +13,9 @@ with Charon and Aeneas, compares complete generated Lean goldens, and proves the inline Rust specifications against both the checked-in and live models. The required `All checks succeeded (ci.yml)` job depends on it. The settled design and deferred work are recorded in [DESIGN.md](DESIGN.md). +The [Aeneas limitations report](AENEAS_LIMITATIONS.md) records encountered +translation and modeling obstacles, their workarounds, and possible upstream +improvements, with current and historical findings distinguished. For application review, start with the ordinary Rust reference calculations and assertion harnesses in [`layout/nested_reference.rs`](../../zerocopy/src/layout/nested_reference.rs),