mwe-unions: MWE for AeneasVerif/aeneas#1199

Three minimal Rust crates exercising the #[repr(C)] union shapes we need Aeneas to support. The examples are progressively more complex and mirror the actual shapes that appear in Linux Binder UAPI structs (see kernel-rust-verification-spike/src/lib.rs).

Each crate is standalone. Each crate's Charon extraction succeeds; each crate's Aeneas run fails at src/llbc/TypesAnalysis.ml:514 with [Error] unions are not supported, followed by a cascade of internal errors on every function that touches the union.

The three cases

Case	Shape	Real-world analogue
A — a-plain-data/	union { u64; u32 } of scalar Copy fields	flat_binder_object__bindgen_ty_1, binder_fd_object__bindgen_ty_1
B — b-tagged-in-struct/	struct { tag: u32, payload: union { ... } }, unsafe { match tag } dispatch	BinderObject + binder_object_header::type_ (reduced to two payload variants)
C — c-byte-array-reinterpret/	union { [u8; N]; u64 } — reinterpret bytes as typed value and back	wire-format overlay pattern in bindgen'd UAPI

Operations we need

• Write one field, read the same field. Cases A, B (per active variant), C. This is not type-punning; it should be as easy to model as a struct.
• Write one field, read another field. Cases A (low32_of_binder), C (u64_from_bytes / bytes_from_u64 / roundtrip). This is the actual type-pun. The #[repr(C)] guarantees it is well-defined; the semantics we care about is bit-level reinterpretation.
• Dispatch on an external tag. Case B (read_active). The caller knows which variant is active from a discriminant carried outside the union.

Reproduce

Environment used in the logs below:

• Aeneas c2015b86 (aeneas-project/aeneas local build).
• Charon 909ff09a (v0.1.220).
• rustc 1.94.0 stable.

for d in a-plain-data b-tagged-in-struct c-byte-array-reinterpret; do
  echo "=== $d ==="
  cd "$d"
  charon cargo --preset=aeneas         # succeeds, produces .llbc
  aeneas -backend lean mwe_unions_${d%%-*}.llbc || true
  cd ..
done

The saved logs are at <case>/aeneas-error.log.

Semantic model we would find sufficient

A byte-array-with-typed-accessors model, extraction-time desugared, is enough for our workload:

union U { a: A, b: B }         ==>       def U := ByteArray N   (N = max(size_of<A>, size_of<B>))
u.a = value_a                  ==>       write_a : U -> A -> U
u.b                            ==>       read_b  : U -> B

with typed accessors emitted as axiomatic functions in the backend (Aeneas.Std.Union.write_field / read_field), documented as implementing the #[repr(C)] layout. Consumers who need functional correctness of type-puns can add invariants themselves; consumers who only need no-panic (our Binder case) get through with a trivial refl on the write-read pattern.

This matches the current shape of how Aeneas treats other type-layout things it does not want to model in-kernel (e.g. size_of, ptr::read_volatile — see AENEAS-REPORT.md).

We are happy with alternatives that give sound write/read/read-other semantics.