vanity

Vanity is an executable model for auditing optimization failures caused by specialization, inlining, and representation lowering.

The project describes a small typed source calculus, lowers it into an explicit target IR, and checks whether source and target observations remain related across pass boundaries. The interesting cases aren't parser or code generation bugs but failures of the abstraction theorem that an optimizer implicitly assumes when it rewrites polymorphic code.

The Idea

The source language keeps representation abstract. It has functions, type abstraction and application, products, sums, recursive types, recursive bindings, and an explicit tick. The effect is intentionally small and just enough to make DCE rewrites observable.

The target IR makes layout explicit. Values can be boxed or unboxed, products and sums have concrete representations, functions carry a boxed or unboxed calling convention, and worker wrapper lowering is represented as a term rather than hidden in the compiler.

The audit asks a simple question at each boundary:

• Did the source and target terminate in the same class?
• Did the effect trace remain equivalent?
• Did representation lowering preserve the selected relation?
• Did the target IR validate its arity and shape constraints?
• Did the pass emit the proof obligation needed to justify the rewrite?

Pipeline

The pipeline is controlled by optimization flags:

type optimisation_flags = {
  specialise : bool;
  inline : bool;
  repr_lower : bool;
  unsafe_repr_eq : bool;
  unsafe_strict_unroll : bool;
  unsafe_effect_drop : bool;
}

Compilation records each intermediate term:

source -> specialise -> inline -> effect rewrite -> repr lower -> target IR

Each pass may also emit obligations:

• Preserve the source relation at a rewrite site.
• Account for exposed representation specific tests.
• Prove that strictness didn't shift termination.
• Preserve effect observations.
• Justify worker wrapper argument and result correspondence.

Safe profiles leave those obligations discharged or merely assumed where the model has no full proof engine. Unsafe profiles deliberately refute them so the failure appears as a small source target delta.

Relations

The comparison engine supports three relations:

• Compare source observations without representation lowering.
• Relate boxed source values to unboxed target values.
• Restrict comparison to ground integer and boolean values.

These relations are intentionally small. The point is to make the failure mode visible, not to model a compiler front end.

Corpus

The checked corpus contains witnesses for both preserved and broken rewrites.

Safe Polymorphic Instantiation

This case instantiates a polymorphic constant function at bool.

forall a. a -> a -> bool

Specialization alone should preserve the baseline relation. No representation specific primitive is introduced, so the free theorem remains intact.

Representation Exposure

This case instantiates the same polymorphic shape at int and then permits an unsafe inline profile to rewrite the abstract branch into eq_int.

The source term is parametric. The target term is no longer parametric because it can observe integer representation.

Strictness Shift

This case places a divergent recursive computation behind a roll boundary.

roll mu a. int loop

A safe lowering keeps the payload latent, while an unsafe unroll path forces it early to change termination.

Effect Shift

This case uses an effectful dead binding:

let _ = tick "alloc" 0 in 1

The result value is independent of the binding, but the observation isn't. Dropping the binding is only valid if the eliminated term is effect free.

Worker Wrapper

This case lowers a boxed pair function through an unboxed worker.

int * bool -> int * bool

The wrapper preserves the boxed source interface while the worker receives RInt and RBool. The target validator checks that worker arity and result shape still match the representation relation.

Notes

• The model is call by value.
• Target validation is structural and representation aware.
• Generated campaigns sample typed source terms and shrink failing specimens.
• Unsafe profiles are supposed to fail; they are witnesses, not broken tests.
• This is a semantic audit harness and not a complete optimizer.