fix: Skip builtin methods in trait impl struct literals

[mennanov]

When a trait impl method is a builtin (e.g. PartialOrd::lt, Ord::max, PartialEq::ne), Aeneas does not emit a def for it — the Lean library provides the implementation. However, extract_trait_impl was still emitting a field reference to the non-existent def in the struct literal, creating a dangling self-reference that Lean cannot resolve.

Now, when iterating over impl.methods, we check whether the method's translated function has builtin_info set. If so, the field is omitted from the struct literal, relying on the default field values added in #940.

Also adds a wrap_lt test exercising derived PartialOrd < on a newtype.

[sonmarcho]

Thanks for looking into this! The fact that the output contains an axiom is a bit suspicious given that there is a model of the default implementation in the Lean library. What is generated without your fix? Looking at this from a distance, my intuition is that we may want to use @[trait_default] and the impl_def elaborator more liberally.

[mennanov]

Thanks for the feedback!

With the current Charon, the output is identical with and without my fix.
The impl method name (order::{core::cmp::PartialOrd<order::Wrap> for order::Wrap}::lt) does not match the builtin pattern (core::cmp::PartialOrd::lt), so builtin_info is None and the check never triggers.

The output in both cases is:

  axiom Wrap.Insts.CoreCmpPartialOrdWrap.lt : Wrap → Wrap → Result Bool

  @[reducible]
  def Wrap.Insts.CoreCmpPartialOrdWrap : core.cmp.PartialOrd Wrap Wrap := {
    partialEqInst := Wrap.Insts.CoreCmpPartialEqWrap
    partial_cmp := Wrap.Insts.CoreCmpPartialOrdWrap.partial_cmp
    lt := Wrap.Insts.CoreCmpPartialOrdWrap.lt
  }

This compiles, but it contains an axiom.

Apparently Charon marks the impl method as opaque in the LLBC (opaque fn order::{core::cmp::PartialOrd<order::Wrap> for order::Wrap}::lt), so Aeneas translates it with body = None.

Btw, on main (without my wrap_lt test function), lt doesn't appear at all: Charon only includes it in the method list when something calls <.

On @[trait_default] + impl_def: The approach you suggest is probably a better long term option while this PR fixes my exact issue i have in my project today (see https://github.com/mennanov/simplex/blob/3e95bab9873632e10f97a271236a0135b9a60606/scripts/gen_lean.sh#L211-L221)

Do you envision smth like this? Plan:

1. Mark the library defaults with @[trait_default] (e.g., core.cmp.PartialOrd.lt.default, core.cmp.Ord.max.default, core.cmp.PartialEq.ne.default)
2. When an impl method is opaque in the LLBC but has a known library default, emit the field using the default (e.g., lt := core.cmp.PartialOrd.lt.default partial_cmp) instead of an axiom, and use impl_def for the struct literal

In theory this should eliminate both the axiom and self-reference issues.
I can try to take a stab at it in a separate PR.

I'll leave it up to you to decide whether it's worth merging this quick fix.