Phase 1, Section 6: Verification Track

Phase 1: Implementation — the shape-typed core compiled end-to-end. Section 6 of 8: Verification Track.

1. What this section commits to

The parallel Lean 4 verification work that runs alongside Phase 1's implementation. Specifically:

• The Lean 4 project layout: structure, dependencies, build orchestration.
• The mechanization plan: which parts of Phase 0 get formalized in Phase 1, and to what fidelity.
• The one non-trivial proof that Phase 1 commits to delivering — subject reduction for an elementwise fragment.
• Translation validation infrastructure as a complement to full mechanization.
• The relationship between the mechanized types in Lean and the OCaml/Rust implementation.
• Acceptance criteria for the verification track specifically.
• What's deferred to Phase 6 (the full verification phase).

This section is deliberately smaller in scope than Sections 2–5. The verification track is parallel to implementation, not on its critical path. Phase 1's verification work is bounded by what's tractable in 4–6 months part-time alongside the rest of the work, not by what's possible in principle.

2. Why Phase 1 has verification at all

The full verified-compilation story is Phase 6. So why does Phase 1 commit to verification work at all?

Three reasons, in order of importance:

1. Mechanization surfaces spec bugs. Translating an English-language specification into Lean 4 forces every ambiguity to be resolved. Phase 0 was written carefully but Phase 0 was English. Mechanizing it in Phase 1 will surface gaps, contradictions, and underspecified cases that English review missed. This is cheaper to discover in Phase 1 (paper revision) than in Phase 6 (after years of implementation built on the spec).

2. The verification track has long lead time. Phase 6's full verified-compilation deliverables (verified subject reduction, verified sharding, verified AD) require infrastructure — a Lean mechanization of the type system, proof tactics tailored to the project, integration between Lean and the OCaml IR. Building this in Phase 1 means Phase 6 starts with infrastructure rather than from scratch.

3. It's a credibility test. Multiple ambitious type-system projects have failed at the proof step — committed to "we'll verify it later" and then discovered the framework was unprovable. Phase 1's commitment to one non-trivial proof is the earliest possible falsification of the verification ambition. If subject reduction for an elementwise fragment is intractable in Lean 4, the whole framework needs revision.

The discipline parallels the bootstrap-and-self-modeling track's AD-as-handler PoC (§6 of that document): a small, early demonstration that the load-bearing thesis works, before the project commits more weight to it.

3. Lean 4 project structure

The Lean 4 project lives at verify/ under the monorepo (per Phase 0 §5.5).

verify/
├── lakefile.lean                       — Lake build manifest
├── lean-toolchain                      — pinned Lean 4 version
├── Verify/
│   ├── Syntax/
│   │   ├── Types.lean                  — type grammar (mechanizing Phase 0 §1)
│   │   ├── Refinements.lean            — refinement language
│   │   └── Expressions.lean            — expression grammar
│   ├── Typing/
│   │   ├── Rules.lean                  — typing judgments (Phase 0 §2)
│   │   ├── Subtyping.lean              — subtyping (Phase 0 §3)
│   │   └── WellFormedness.lean         — type formation rules
│   ├── Semantics/
│   │   ├── Values.lean                 — values and tensors-as-functions (Phase 0 §4)
│   │   ├── Reduction.lean              — small-step reduction
│   │   └── Heap.lean                   — the heap model
│   ├── MetaTheory/
│   │   ├── SubjectReduction.lean       — THE Phase 1 proof goal (elementwise fragment)
│   │   ├── Progress.lean               — Phase 6 goal; statement only in Phase 1
│   │   └── Soundness.lean              — Phase 6 goal; statement only in Phase 1
│   └── TranslationValidation/
│       ├── ObligationFormat.lean       — what compiler-emitted obligations look like
│       └── Discharge.lean              — minimal discharge infrastructure
└── test/
    ├── TypingExamples.lean             — small typing examples in Lean
    └── ReductionExamples.lean          — small reduction traces

Five top-level sub-libraries: Syntax, Typing, Semantics, MetaTheory, TranslationValidation. The structure mirrors Phase 0's section organization; this is deliberate — the mechanization tracks the spec section-by-section.

3.1 Dependencies

-- lakefile.lean
require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "<pinned-tag>"

mathlib is the standard Lean 4 mathematics library. We need it for:

• Number theory (for the Presburger arithmetic encoding).
• Order theory (for the refinement-language semantics).
• Basic set theory (for typing contexts).

Pinning to a specific tag, with deliberate-cycle upgrades, per Phase 0 §5.7's pinning discipline.

3.2 Build integration

The Lean 4 build is part of CI (per Section 7's testing infrastructure). Every push that touches verify/ triggers a Lean build; failures are PR-blocking. This means the mechanization stays current — the spec and the mechanization can't diverge silently.

A single lake build command builds the whole verify/ tree; failures point to specific files.

4. Mechanization plan

What gets formalized in Phase 1, and at what fidelity.

4.1 Three fidelity levels

4.2 What Phase 1 formalizes

Phase 0 Section 1 (Type System Foundation): mechanized with most proofs.

The grammar of types, refinement language, and type formation rules. Most accompanying lemmas (well-formedness preservation, refinement-language soundness with respect to integer arithmetic) are provable in Phase 1.

Phase 0 Section 2 (Operations and Typing Rules): mechanized statements; selective proofs.

All ten core operations from Phase 0 §2 (including both reduce typing rules) plus the four extensions from Section 5 of this Phase 1 spec are mechanized as inductive cases of the typing relation. The typing rules are stated. Proofs (e.g., that the typing relation is decidable) come in Phase 6 except for the elementwise fragment.

Phase 0 Section 3 (Subtyping): mechanized statements; basic proofs.

The subtyping relation is mechanized. Reflexivity and transitivity are provable in Phase 1 (mechanical). The bidirectional algorithm's correctness is stated; proof deferred to Phase 6.

Phase 0 Section 4 (Operational Semantics): mechanized statements; no proofs in Phase 1.

The reduction relation and value definitions are stated. Subject reduction is the Phase 1 proof goal (§5 below). Progress is stated; proof deferred to Phase 6.

Phase 0 Section 5 (Implementation Infrastructure): not formalized.

Section 5 is engineering rather than formal content. Nothing to mechanize.

4.3 The mechanization is partial by design

A Phase 1 user inspecting the verify/ tree finds many sorry placeholders. This is intentional. Phase 1 commits to:

• Every Phase 0 §1–§4 definition has a Lean counterpart.
• Every typing rule has an inductive case.
• Every meta-theorem has a stated theorem (possibly with sorry).
• At least one non-trivial theorem is fully proved.

The remaining proofs are Phase 6 work. Phase 1's commitment is to the infrastructure that makes those proofs tractable, not to the proofs themselves.

5. The first non-trivial proof: subject reduction for the elementwise fragment

The single load-bearing deliverable of the verification track in Phase 1.

5.1 The theorem

theorem subject_reduction_elementwise
    (Γ : TypingContext) (e e' : Expr) (τ : Type)
    (h_typed : Γ ⊢ e : τ)
    (h_step : e ⟶ e')
    (h_elementwise : isElementwiseFragment e) :
    Γ ⊢ e' : τ

In English: if e is in the elementwise fragment of the language and well-typed at type τ, and e reduces to e', then e' is also well-typed at τ.

5.2 What "elementwise fragment" means

The fragment is restricted to:

• Tensor literals (constants).
• Variable references.
• Let-bindings (sequencing).
• Unary elementwise operations (per Phase 0 §2).
• Binary elementwise operations (per Phase 0 §2).
• Reduce operations along a single axis.

Excluded from the fragment:

• Matmul (preserves typing but the proof is more involved).
• Reshape (the volume-axiom controlled-unsoundness complicates the proof).
• Broadcast, slice, concat, transpose (preserve typing but more cases).
• Function calls and polymorphic instantiation (substitution lemmas needed first).

The fragment is deliberately small. The point is to demonstrate that the proof infrastructure works, not to cover everything. Phase 6 extends the proof to the full operation set.

5.3 Why this fragment

Three properties:

1. It's tractable. The fragment has well-understood proof techniques in Lean — most cases are direct from the rule shapes.
2. It exercises the framework. Subject reduction for elementwise operations requires the type-formation rules, the refinement-language semantics, the reduction rules, and basic substitution. If Phase 1's mechanization can't support this proof, the framework is unprovable.
3. It's a non-trivial result. "Subject reduction for an elementwise fragment" is a real meta-theorem, not a triviality. A working proof gives Phase 1 something tangible to point to: the type system is provably sound, at least on this fragment.

5.4 Proof strategy

Standard induction on the typing derivation. For each typing rule case, examine which reduction step could fire and verify the resulting expression is still well-typed. The non-trivial cases are:

• Reduce-along-axis with refinement obligations involving the reduction's effect on shape variables. The proof shows the obligations remain dischargeable after reduction.
• Binary with broadcasting. Phase 0 §2.11 forbids implicit broadcasting; the broadcasting is an explicit operation. The proof shows the explicit broadcast preserves typing through reduction.

Estimated proof size: 200–400 lines of Lean. Substantial but tractable. Comparable to similar fragments in the literature (Pierce's "Software Foundations" formalization of STLC subject reduction is in this size range).

5.5 What if it doesn't work

If the proof is intractable — if specific cases require lemmas that don't go through, or the framework's encoding makes the proof artificially difficult — that's a Phase 1 finding. The response options:

1. Reformulate the encoding. Most often the issue is how the types or rules are stated in Lean; reformulating fixes it.
2. Strengthen the typing rules. Sometimes the spec needs revision — a typing rule too permissive blocks the proof. Phase 0 revision.
3. Reduce the fragment further. If subject reduction for unary + binary works but reduce doesn't, the Phase 1 proof commits to the smaller fragment. Acceptable; honest.
4. Conclude the framework is wrong. If even the smallest non-trivial fragment can't be proven, that's a foundational issue. The response is the abandonment-or-revision conversation from Section 1 §6.3.

The discipline is the same as everywhere else: a wrong outcome triggers a decision, not slow drift.

6. Translation validation infrastructure

A complement to full mechanization. Different in approach, different in scope, but mutually reinforcing.

6.1 The idea

Full mechanization proves "the compiler is correct on all programs" once and for all. Translation validation proves "the compiler is correct on this specific program" each time. The latter is more tractable per-program but doesn't generalize; both are useful.

For Phase 1:

• Full mechanization gives us the elementwise-fragment subject reduction (§5).
• Translation validation gives us per-program proofs that the compiler's output preserves typing (a weaker property than subject reduction but easier to discharge).

6.2 What translation validation produces

For each program the compiler processes, an obligation file:

program: matmul.sexp
obligation: ∀ (input : Tensor[F32, [B, M, K]]),
              let output = compile(matmul.sexp)(input) in
              output : Tensor[F32, [B, M, N]]

The obligation is then discharged by the verification toolchain. Phase 1's discharge can be:

• Trusted (the compiler asserts the obligation; Phase 1 default).
• Heuristic (lightweight checks like type re-inference on the output IR).
• Z3-discharged (translate the obligation to SMT; not Phase 1).
• Lean-discharged (translate to Lean 4 and prove; Phase 6).

Phase 1 implements the infrastructure for these obligations — the format, the obligation generator, the discharge framework — without committing to a non-trivial discharge mechanism. The trusted mode and heuristic mode are sufficient for Phase 1.

6.3 Why this matters in Phase 1

Even without a real discharge mechanism, the obligation format is load-bearing. It forces:

• The compiler to track exactly what it claims about each output.
• The IR to expose typing information at every stage of lowering.
• The runtime to know what it's running (for diagnostic context).

These are Phase 1 disciplines that bear no immediate cost but pay off heavily in Phase 6. Same pattern as the runtime FFI design (Section 3 §6.1) and the DLPack ABI prefix (Section 3 §5).

7. Relationship to the OCaml/Rust implementation

Three points where the verification work touches the implementation:

7.1 The mechanized types are the source of truth for the spec

When the OCaml types in compiler/lib/ir/types.ml and the Lean types in verify/Verify/Syntax/Types.lean disagree, the Lean version is canonical. The OCaml side is implementation; the Lean side is specification.

Practically: when a Phase 0 §1 detail comes up during implementation work and the spec is ambiguous, the resolution is to consult the mechanization first (or, if not yet mechanized, to mechanize the resolution). This keeps the spec living rather than letting it stagnate.

7.2 Translation validation obligations come from the compiler

The compiler emits obligation files (in the format from §6.2) as a side effect of compilation. The discharge tooling lives in verify/. The compiler's elaboration pipeline (Section 2 §5) gains a small obligation-emission stage; the verification track consumes the output.

7.3 Test programs are shared

The compiler/test/fixtures/ directory (per Section 2's project structure) contains test programs. These programs are also typing examples in verify/test/TypingExamples.lean — the same programs, examined from both implementation and verification perspectives. When a test program changes, both sides update.

This sharing makes divergence visible: a program that compiles via OCaml but doesn't type-check in Lean (or vice versa) is a real bug, surfaced quickly.

8. Implementation milestones (verification-specific)

The verification work spreads across Phase 1's three milestones:

8.1 Milestone 1 (months 1–2): infrastructure

• Lean 4 project bootstrapped: lakefile.lean, lean-toolchain, mathlib dependency.
• Phase 0 §1 (types, refinements) mechanized as Lean definitions.
• Phase 0 §1 type-formation rules mechanized; basic well-formedness lemmas proven.
• CI integration: lake build runs on every push; failures are PR-blocking.

This milestone is mostly translation work — turning Phase 0's English into Lean 4 syntax. Few proofs, lots of definitions.

8.2 Milestone 2 (months 3–4): rules and reduction

• Phase 0 §2 typing rules mechanized as the ⊢ inductive relation.
• Phase 0 §3 subtyping mechanized; reflexivity and transitivity proven.
• Phase 0 §4 reduction rules mechanized as the ⟶ relation.
• Translation validation obligation format committed to.

By end of Milestone 2, the framework is in place. The subject reduction theorem statement exists; its proof is Milestone 3 work.

8.3 Milestone 3 (months 5–6): the proof

• Subject reduction for the elementwise fragment fully proved (no sorry).
• Documentation: a walkthrough of the proof for future contributors.
• Translation validation infrastructure with a working trusted-mode example.
• Phase 6 entry conditions documented.

Milestone 3's proof is the load-bearing deliverable. Everything else is supporting infrastructure.

9. Acceptance criteria

The single load-bearing criterion is the elementwise subject reduction proof goes through. Everything else is infrastructure that can be incomplete without invalidating the project; this one proof is the empirical evidence that the framework is provable.

10. Open issues and future scope

10.1 Open issues for Phase 1

1. The Presburger encoding in Lean. Phase 0 commits to quantifier-free Presburger arithmetic, with Z3 as the discharge engine. Mechanizing this in Lean has options: rely on mathlib's number theory; encode Presburger natively as a small DSL; defer to Lean's omega tactic (which decides linear arithmetic over integers). Phase 1 commits to omega first, custom DSL second — start with the standard library, only build custom infrastructure if omega proves insufficient.

2. The Z3 connection. The OCaml compiler discharges refinement obligations with Z3 (per Section 2 §6). The Lean mechanization could either (a) reproduce the SMT logic in Lean via omega and similar tactics, or (b) trust Z3's results in the Lean proofs (axiomatize SMT). Phase 1 commits to (a) — the proofs go through in Lean's own logic. Cross-referencing Z3 and Lean is Phase 6 work.

3. The relationship between Lean types and OCaml IR types. The two need to stay in sync. The discipline (per §7.1) is "Lean is canonical." But OCaml has features (modules, polymorphic variants) Lean lacks; Lean has features (dependent types, propositional equality) OCaml lacks. Some translation friction is inevitable. Worth flagging that this friction is a real cost; documented but not solved.

10.2 Phase 6 deferred work

What Phase 1 does not deliver, by design:

• Subject reduction for the full operation set. Phase 1's proof covers an elementwise fragment. The full proof (matmul, reshape, broadcast, etc.) is Phase 6.
• Progress (the second half of type soundness — well-typed terms either are values or can take a step). Phase 1 states it; Phase 6 proves it.
• Bidirectional type-checking correctness. The algorithm in Section 2 §5.2 is stated in Lean; its correctness with respect to the typing relation is Phase 6.
• Verified compilation passes. Each compiler pass producing a typing-preserving output is a separate proof. Phase 6 territory.
• Verified AD. The AD-as-handler (per the bootstrap track) gets verified in Phase 6.
• Numerical accuracy bounds. Phase 0 §4.6 separates structural typing from numerical accuracy; bounds on FP error are Phase 6.

The Phase 6 work plan, when written, will be a follow-on to Phase 1's verification track. Phase 1's deliverables make Phase 6 tractable; they don't replace it.

11. Section 7 preview

Section 7 covers Testing, Quality, and Public ABI — the cross-cutting concerns that ensure Phase 1's deliverables are reliable and consumable. Specifically:

• The CI strategy: unit tests, integration tests, GPU tests, golden-output tests against PyTorch.
• Performance regression infrastructure (using the observability instrumentation from Section 4).
• The public ABI stability discipline: which surfaces are stable, which are unstable, the path between them.
• The library author's guide (the first version, per the ecosystem-architecture forward track).
• Documentation requirements.

After Section 7, only the exit criteria (Section 8) remain.

End of Phase 1, Section 6.