Prove FromBytes and FromZeros construction invariants

tools/aeneas-inline/src/main.rs

@@ -241,7 +241,10 @@ impl Functions<'_> {
         if let syn::ReturnType::Type(_, ty) = &sig.output {
             supported &= !unsupported_borrow(ty, false);
         }
-        let (bounds, bounds_supported) = trait_bounds(&sig.generics);
+        let (bounds, bounds_supported) = trait_bounds_with_context(
+            &sig.generics,
+            if method { &self.impl_generics } else { &[] },
+        );
         supported &= bounds_supported;
         let mut generics = if method { self.impl_generics.clone() } else { Vec::new() };
         for parameter in &sig.generics.params {
@@ -304,6 +307,10 @@ fn declaration_start(
 // These spellings propose source ownership only. The compiler's resolved
 // predicates, not names from syn, decide which trait dictionary is required.
 fn trait_bounds(generics: &syn::Generics) -> (Vec<Value>, bool) {
+    trait_bounds_with_context(generics, &[])
+}
+
+fn trait_bounds_with_context(generics: &syn::Generics, context: &[String]) -> (Vec<Value>, bool) {
     fn bound(subject: &str, bound: &syn::TypeParamBound) -> Option<Value> {
         let syn::TypeParamBound::Trait(bound) = bound else { return None };
         if bound.lifetimes.is_some()
@@ -345,7 +352,8 @@ fn trait_bounds(generics: &syn::Generics) -> (Vec<Value>, bool) {
                 continue;
             };
             supported &= predicate.lifetimes.is_none()
-                && generics.type_params().any(|p| p.ident == *subject);
+                && (generics.type_params().any(|p| p.ident == *subject)
+                    || context.iter().any(|name| subject == name));
             for predicate in &predicate.bounds {
                 match bound(&subject.to_string(), predicate) {
                     Some(value) => bounds.push(value),
@@ -729,6 +737,31 @@ impl<'ast> Visit<'ast> for Functions<'_> {
             "supported": self.unsupported == 0 && item.generics.params.is_empty()
                 && item.generics.where_clause.is_none(),
         }));
+        // A provided method owns a real function body. Its implicit Self type
+        // and enclosing trait come from this item, not from a guessed path.
+        // Report these bodies separately so their specs receive the same
+        // closed annotation census as free functions and inherent methods.
+        let previous_generics = self.impl_generics.clone();
+        self.impl_generics = std::iter::once("Self".to_string())
+            .chain(item.generics.type_params().map(|p| p.ident.to_string()))
+            .collect();
+        self.modules.push(item.ident.to_string());
+        for member in &item.items {
+            if let syn::TraitItem::Fn(method) = member {
+                if let Some(body) = &method.default {
+                    self.function(
+                        &method.sig,
+                        body,
+                        &method.attrs,
+                        true,
+                        &syn::Visibility::Inherited,
+                    );
+                    self.functions.last_mut().unwrap()["default_trait"] = json!(path.join("::"));
+                }
+            }
+        }
+        self.modules.pop();
+        self.impl_generics = previous_generics;
         self.unsupported += 1;
         visit::visit_item_trait(self, item);
         self.unsupported -= 1;
@@ -909,6 +942,23 @@ mod tests {
         }
     }
 
+    #[test]
+    fn provided_method_retains_enclosing_self_in_where_clauses() {
+        let value = inspect(
+            "mod nested { unsafe trait Marker { fn required();
+                fn make() -> Self where Self: Sized { panic!() }
+            } }",
+        )
+        .unwrap();
+        let functions = value["functions"].as_array().unwrap();
+        assert_eq!(functions.len(), 1);
+        assert_eq!(functions[0]["path"], "nested::Marker::make");
+        assert_eq!(functions[0]["default_trait"], "nested::Marker");
+        assert_eq!(functions[0]["generics"], json!(["Self"]));
+        assert_eq!(functions[0]["trait_bounds"], json!([{"subject": "Self", "trait": "Sized"}]));
+        assert_eq!(functions[0]["supported"], true);
+    }
+
     #[test]
     fn borrow_policy_distinguishes_shared_inputs_from_outputs_and_fields() {
         for (ty, input_supported) in [

verification/aeneas/LOWERING_AUDIT.md

@@ -224,6 +224,35 @@ trait objects. A missing child representation remains unavailable through its
 wrapper; an available child decoder must carry its actual correspondence and
 initialization premise.
 
+### Zero construction and construction-trait laws
+
+`FromBytes` and `FromZeros` consume the same decoder-correspondence premises
+above. Their additional mathematical decoding condition records library
+validity, rather than treating bit validity as sufficient for every invariant.
+The selected nine impl proofs cover unit, u8, u32, Boolean zero construction,
+and generic arrays. They do not certify the other construction-trait impls.
+
+The `core::mem::zeroed` interpretation uses the selected provider's physical
+width, all initialized zero bytes, and that provider's mathematical decoder.
+Applying it to Rust additionally assumes the selected physical interpretation
+has the actual Rust width and represents the resulting Rust value. The existing
+primitive and array premises supply that connection for the concrete proofs;
+compiler assertions challenge unit, Boolean, byte, u32, and representative array
+widths. A successful construction does not assert that initialized padding
+survives a typed move. The current resource-free scope adds no claim about
+provenance, ownership, destruction, or external-state constructor permission.
+
+A checked semantic provider suffix extends generic native definitions that use
+this boundary. It does not replace their extracted computation or Rust input
+prefix. Both the native call audit and the independently written outcome family
+retain that provider before choosing an outcome. The exact enclosing trait
+bound, if Charon removes it from a default body's computational arguments, is
+recovered as a specification premise from original trait/method ownership.
+Required pointer-based validators are signature-only dictionary fields: their
+whole Lean stubs return undef, and admission rejects every execution of them.
+Their opaque Ptr carrier is an audited type constructor, not a value, spatial
+model, or proof axiom about pointers.
+
 ### Empty construction and external invariants
 
 Size zero does not imply that a value exists, that a Rust constructor may be

verification/aeneas/README.md

@@ -505,8 +505,10 @@ The marker has no name or proposition: the Rust header identifies the trait,
 carrier, and generic bounds. Its proof must cover every original type and const
 parameter using only those bounds and their model providers. CI binds the marker
 to its compiler owner. The source census retains inactive and unused source
-and checks reserved annotations in macro templates too. Conditional, computed,
-inner, misplaced, and unsupported forms fail explicitly. The complete native
+and checks reserved annotations in macro templates too. Conditional or computed
+annotations, inner annotations, misplaced annotations, and unsupported forms
+fail explicitly. Computed ordinary documentation may accompany a literal
+annotation; the expanded census must still account for every reserved fence. The complete native
 HIR attribute census reconciles physical source origin, decoded doc text,
 fragment order, and multiplicity; direct markers also retain their declaration,
 signature, body, and source checks. Native evidence is recorded in
@@ -524,8 +526,9 @@ the trait's promise. It cannot prove that a future downstream impl keeps that
 promise. Each selected local impl has a separate ordinary theorem discharging
 the promise, and Rust's unsafe-trait contract remains the obligation of external
 implementers. CI also inspects every extracted
-implementation method body in the original and final ASTs, even when only the
-law refers to the method.
+admitted implementation method body in the original and final ASTs, even when
+only the law refers to the method. Excluded provided methods cannot execute;
+interface-only validators retain their required signatures but cannot be called.
 
 This initial bridge accepts traits with only their `Self` parameter and simple
 generic bounds. It compares compiler-resolved original and final type
@@ -784,6 +787,49 @@ pointer provenance, destruction, or general Rust UB-freedom.
 is outside these laws. See [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining
 lowering boundaries.
 
+## `FromBytes`, `FromZeros`, and owned zero construction
+
+The `FromBytes` law requires every fully initialized byte sequence of the
+physical decoder's exact width to produce both a language-valid raw value and
+a mathematical value. The `FromZeros` law requires the same two stages for the
+all-zero sequence. Both stages use one `RustModel` provider; a physical success
+cannot bypass an optional library invariant. A missing physical decoder fails
+both laws. These definitions permit padding: neither law promises that a typed
+copy preserves the initialized padding bytes used for construction.
+
+Nine `invariant_proof` markers cover `()` and `u8`/`u32` for both traits,
+`bool` for `FromZeros`, and the two generic array impls. Array proofs compose
+the actual element decoder and its law, including empty arrays and zero-sized
+elements. The completeness lemma also derives the zero law from a `FromBytes`
+law. Negative Lean examples distinguish Boolean zero validity from Boolean
+validity for every byte, and reject zero construction of nonzero integers or a
+value rejected by its library decoder.
+
+Aeneas normally has no model dictionary in the computation. The downstream
+`native_models` elaborator retains a provider only in generic definitions
+whose bodies need this boundary. Original Rust arguments remain in their exact
+order, followed by implicit semantic providers; anonymous lets retain unused
+arguments without changing the body. Contracts reuse those same providers.
+They cannot quantify a different decoder after choosing an execution outcome.
+The native-input audit distinguishes this checked suffix from source arguments.
+
+Charon can erase the unused enclosing Self dictionary from a default body.
+Source and compiler evidence identify its trait and method slot before that
+erasure; the specification receives that exact trait dictionary and law as
+premises. These are specification parameters, not replacements for Rust
+arguments. Separately, required `TryFromBytes::is_safe` fields retain their
+native signatures but have no execution model. Carrying those dictionaries is
+allowed; calling an unmodeled validator is rejected at admission. Its opaque
+`Ptr` carrier supplies no construction, layout, provenance, or validity facts.
+
+As with `IntoBytes`, applying these proofs to Rust assumes the physical decoder
+has the correct Rust width and language meaning. The primitive and array
+interpretations have explicit Reference premises; compiler assertions challenge
+the concrete widths. A generic provider is a supplied interpretation, not a
+proof of an arbitrary downstream type's representation. These construction laws
+cover the selected impls; they do not certify pointer access, external-state
+invariants, destructors, or every `FromBytes`/`FromZeros` impl.
+
 ## Native Lean proofs and independent checks
 
 `Specs.lean` is generated from the Rust comments in a fixed context containing