Discharge the opaque size_of axiom: a typeclass model that also makes the sizes checkable

Compara la rama spike-typeclass con la línea base 851cade9 y, después, inspecciona NoPanic.lean, los archivos generados y los enunciados de los teoremas afectados. Ejecuta lake build y la auditoría de axiomas; se considera terminado cuando el axioma opaco size_of está ausente, los hechos sobre el tamaño siguen siendo comprobables y la compilación existente tiene éxito.

Title:

Discharge the opaque size_of axiom: a typeclass model that also makes the sizes checkable

Body:

Your README lists this under Next:

Discharge the opaque size_of axiom (model core.mem.size_of as a concrete constant) so parse_one_no_panic depends only on the standard Lean axioms.

Done, and the "concrete constant" part works better than I first thought.
Branch: https://github.com/repowazdogz-droid/kernel-rust-verification-spike/tree/spike-typeclass

Happy to open a PR against main if you want it.

Result. Baseline at 851cade9, Lean 4.31.0, Aeneas c2015b86. Before: 'parse_one_no_panic' depends on axioms: [propext, Classical.choice, Quot.sound, spike_binder_remodel.core.mem.size_of]. After: [propext, Classical.choice, Quot.sound], and the same for parse_one_no_panic_uncond, size_of_binder_buffer_object, type_to_size_ptr. lake build completes successfully, 1702 jobs.

The change. A RustSized class carrying a Std.Usize, core.mem.size_of (T : Type) [inst : RustSized T] := ok inst.size under the same @[rust_fun], and five instances (flat 24, fd 24, buffer 40, fd_array 32, Std.Usize 8). @[rust_fun] accepts the instance argument, and your generated call sites elaborate unchanged by instance synthesis, so I did not have to touch a single call site.

What this buys beyond removing the axiom. type_to_size now computes, so the sizes are provable rather than assumed: size_of_binder_buffer_object ... := rfl and type_to_size_ptr : type_to_size BINDER_TYPE_PTR = ok (some 40#usize). These are a regression gate, not documentation. If someone edits an instance to a wrong value they fail to compile; I checked by setting it to 99#usize and pasting the error. The proofs also get shorter. One more thing falls out: ptr_align's size-related obstruction is discharged. The sorry at NoPanic.lean:88 stays, because its Try-trait obstruction is untouched, but one of the three you listed is gone.

What it costs. hsz : ∀ T, ∃ n, core.mem.size_of T = ok n no longer elaborates (failed to synthesize instance of type class RustSized T), so the affected statements drop it. That is a net simplification, but the diff touches your theorem statements, not only the generated files. A type used at size_of without an instance is now a build error rather than a silent assumption, which I think is the behaviour you want, though it is a change in failure mode.

Where the size facts live, and what they actually check. The no-panic theorems do not depend on the sizes at all. I confirmed this before building the typeclass version: with ok 0#usize for every type, the whole thing still builds and the axiom audit is byte-identical. parse_one builds every branch and returns an Err value rather than failing, so no-panic is insensitive to what type_to_size returns. So the value lemmas are not load-bearing for parse_one_no_panic, and I am not claiming they strengthen it. What they do is give the layout facts a checkable home rather than leaving them implicit. The authority for the sizes stays where you already put it, the const _: () = { assert!(...) } blocks in the Rust, which is the right place because that is where the real #[repr(C)] types are. The Lean lemmas mirror those assertions so drift is a build failure on the Lean side too. For what it is worth I re-derived the numbers from include/uapi/linux/android/binder.h (blob 701cad36de43a4743d0f2c1b6ff8132dccc16bd5) rather than copying yours. I get flat 24, fd 24, buffer 40, fd_array 32.

Two caveats. The patch edits generated files, so re-extraction overwrites it. The durable fix is a @[rust_fun "core::mem::size_of"] model in the Aeneas standard library, and there is no such registration under backends/lean/Aeneas/. Given Nadrieril's note on #1199 that Aeneas has no model of layouts or byte representations, a RustSized-style class may be a reasonable shape to propose upstream. There is also a fallback on branch discharge-size-of-axiom that removes the axiom without altering the signature, using opaque rustSizeOf. That needs no instances and no edits to your theorem statements, but proves nothing about the sizes. I would use the typeclass version and am offering the other only in case you would rather keep the signature exactly as Aeneas emits it.