Reject unsupported execution effects before Aeneas lowering

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.
+  <!-- FIXME: Typed transfers lose storage events; track support at
+  https://github.com/AeneasVerif/aeneas/issues/1405. Until then, a typed storage
+  abstraction must forget all padding contents and initialization facts. It
+  must still check access obligations and reject reads that rely on those facts. -->
 - **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

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