Aiur verified-compiler proof scaffolding

[arthurpaulino]

Summary

End-to-end Lean proof scaffolding for the Aiur compiler pipeline, landing Aiur.Toplevel.compile_correct modulo 16 named axioms sitting next to the theorems they replace. Build is green, no sorrys, no warnings.

Pipeline

Source.Toplevel
  ├── mkDecls          → Source.Decls
  ├── checkAndSimplify → Typed.Decls
  ├── concretize       → Concrete.Decls
  ├── lower            → Bytecode + preNameMap
  └── deduplicate      → Bytecode + remap

compile_correct composes three top-level lemmas:

1. compile_progress_entry (Progress)
2. compile_preservation_entry (Preservation)
3. compile_correct_concRetFnFree_entry (FnFree projection)

Organization

• Ix/Aiur/Semantics/ — semantic predicates and evaluator definitions (WellFormed, TypedEval, ConcreteEval, DrainInvariants, Relation, etc.). Anything that defines what a program means.
• Ix/Aiur/Proofs/ — proof modules. Proof-internal predicates kept in self-contained contexts; cross-cutting predicates lifted into Semantics/.
• Each remaining axiom lives in the file of its consumer theorem, declared at the dispatch site with a closure-plan docstring (file/line target, closure path, infrastructure to reuse, dependency notes, LoC estimate, risk factors).

Cross-evaluator value bridging

The cross-evaluator value bridge is carried by ValueR (in Proofs/Simulation.lean), routing concrete-eval ctors at polymorphic-mangled keys (e.g. Option_U32.None) to source ctors with no same-key preimage. The TermBridge.app constructor carries a name-map witness
(concretizeName g_src tArgs = g_conc ∨ same-key).

Axioms (16)

Each axiom is grouped by the file where it lives, with its consumer theorem.

Proofs/LowerSoundControl.lean

• interp_preserves_ValueHasTyp
• Function_body_preservation_succ_fuel

Proofs/ConcretizeSound/Layout.lean

• dataTypeFlatSize_bound_saturation_wf

Proofs/ConcretizeSound/SizeBound.lean

• Global.toString_init
• dt.params parser-shape invariant
• MonoShape projection
• spine_transfer_aux .tuple arm
• spine_transfer_aux .array arm
• spine_transfer_aux .app mono-hit arm
• mkParamSubst_some_implies_param

Proofs/CompilerProgress.lean

• body_compile_ok
• function_compile_progress_entry

Proofs/StructCompatible.lean

• typFlatSize_eq_typSize_under_match_wf (CLOSED — kept named)
• compile_ok_implies_struct_compatible_of_entry

Proofs/Simulation.lean

• step_R_preservation_applyGlobal

Proofs/CompilerCorrect.lean

• body_termBridge_at_function_key

Invariants

1. Wiring discipline — every theorem in Ix/Aiur/Proofs/*.lean (except compile_correct) is transitively reachable from compile_correct. Orphan-free.
2. No body sorries — every remaining work-unit is a named axiom with a sig + closure docstring sitting next to its consumer.
3. Sig stability — axiom signatures are locked; sig changes require explicit amendment documented in the axiom's docstring.

Stats

• ~59 files changed, ~64k insertions
• 277 build jobs green
• 0 sorries, 0 warnings
• 16 axioms, each with closure docstring

Test plan

• lake build green
• No sorry reachable from compile_correct
• No warnings
• Orphan check: every Proofs theorem reaches compile_correct