YOLO

YOLO is the fast, lazy proof-automation backend for SPLean, a Lean 4 separation-logic framework. It targets goals of the form

H1 ==> H2

where H1 and H2 are heap propositions (hProp). Instead of immediately constructing a full Lean proof, YOLO first runs an unverified simplification pass over a compact internal syntax tree, records the tactic script that would justify the simplification, and can later replay that script for proof reconstruction. This is the implementation artifact for the paper "Lazy Proof Automation for Separation Logic".

The main implementation is in SPLean/Extra/NWO.lean. The older xsimp automation lives in SPLean/Theories/XSimp.lean, and the user-facing xsimp' wrapper is wired in SPLean/Theories/WP1.lean.

Build

lake exe cache get
lake build

Running The Automation

Most proofs call xsimp', not hMain directly. The two options below select which backend `xsimp' uses:

-- Baseline verified automation.
set_option hsimp.verify true
set_option hsimp.yolo false

-- YOLO fast phase: simplify and record a reconstruction script.
set_option hsimp.verify false
set_option hsimp.yolo true

-- YOLO proof reconstruction: replay the recorded script.
set_option hsimp.verify false
set_option hsimp.yolo false

Experiments often use:

init_xsimp_time
-- proof ...
get_xsimp_time

Hover over or inspect the get_xsimp_time message to see the accumulated time spent in simplification.

How YOLO Represents Heap Propositions

YOLO does not simplify Lean expressions directly. It parses hProp expressions into:

inductive hprop (α : Type) where
  | hop (op : α) (args : List (hprop α)) : hprop α

The type parameter α is an extensible sum of operation tags. The default tag set used by hMain is:

TStar ⊕ TWand ⊕ TPure ⊕ TEmp ⊕ TAtomic ⊕ TTop ⊕ TForall ⊕ TExists

The built-in tags mean:

• TStar: separating conjunction, stored n-arily by flattening HStar.hStar.
• TWand: separating implication / wand.
• TPure: pure propositions, ⌜p⌝.
• TEmp: empty heap, emp.
• TTop: top heap proposition, ⊤.
• TExists, TForall: heap-level binders.
• TAtomic: fallback wrapper for heap atoms not otherwise recognized.

The simplifier state partitions the entailment into left/right worklists:

structure hState_ (α : Type) where
  hla : List (hprop α) -- accumulated LHS atoms
  hlw : List (hprop α) -- accumulated LHS wands
  hlt : List (hprop α) -- LHS todo
  hra : List (hprop α) -- accumulated RHS atoms
  hrg : Bool           -- RHS has top 
  hrt : List (hprop α) -- RHS todo
  tacticScript : Array Syntax

Each operation tag teaches YOLO four things:

• how to parse a Lean expression into an hprop node;
• how to print an hprop node back to a Lean expression;
• when two nodes are definitionally equal for cancellation;
• how the node behaves when processed on the LHS, RHS, inside a wand, or at the final LHS/RHS phase.

Those pieces are expressed as typeclasses in SPLean/Extra/NWO.lean.

Adding A New YOLO Operation

There are two levels of extension.

Use an expression handler when your operation is still an ordinary atomic heap predicate and you only want special cancellation/keeping behavior. This is what the built-in hsingle optimization does.

Use a new operation tag when the predicate has real structure that should be visible to the simplifier, or when you need custom LHS/RHS/wand/final behavior. That is the important path.

1. Define A Tag

Create a small structure carrying exactly the data YOLO needs to reconstruct the heap predicate. For example, suppose we have a heap predicate:

def hcell2 (p : loc) (v w : val) : hProp := ...

Add a tag:

structure TCell2 where
  p : Expr
  v : Expr
  w : Expr

instance : Inhabited TCell2 where
  default := ⟨default, default, default⟩

The fields are Lean.Expr because YOLO runs after elaboration.

2. Reconstruct Lean Expressions: ToExprT

Implement ToExprT so a simplified hprop can be turned back into a Lean goal.

instance : ToExprT TCell2 where
  toExpr x args := do
    -- Use args when the operation has recursive hprop children.
    -- Here hcell2 is atomic, so args should be empty.
    mkAppM ``hcell2 #[x.p, x.v, x.w]

For binder-like or connective-like operations, consume args and build the corresponding expression from them. See the TWand, TStar, TExists, and TForall instances in NWO.lean.

3. Parse Lean Expressions: HasToHprop

Teach Expr.toHprop how to recognize the predicate. If you skip this step, the predicate will be wrapped as TAtomic, and your custom Eval TCell2 ... instance will never run.

partial def cell2ToHprop {γ : Type} [Embed TCell2 γ]
    (e : Expr)
    (f : Expr → hprop γ)
    (go : Expr → List (hprop γ))
    : Option (hprop γ) :=
  match_expr e with
  | hcell2 p v w =>
      some (hprop.hop (Embed.inj (TCell2.mk p v w)) [])
  | _ =>
      none

instance [Embed TCell2 γ] : HasToHprop TCell2 γ where
  toHprop := [cell2ToHprop]
  toHpropGo := []

The Embed TCell2 γ constraint lets this parser work for any larger sum of operations that contains TCell2.

4. Define Cancellation Equality: TIsDefEq

YOLO cancellation uses TIsDefEq, not plain BEq. Use Meta.isDefEqAssign when metavariables should be assigned during matching.

instance [Embed TCell2 γ] : TIsDefEq TCell2 γ where
  isDefEq x y isArgsEq := do
    match matchExpr y with
    | some y =>
        let okP ← Meta.isDefEqAssign x.p y.p
        let okV ← Meta.isDefEqAssign x.v y.v
        let okW ← Meta.isDefEqAssign x.w y.w
        return okP && okV && okW && isArgsEq
    | none =>
        return false

For an atomic operation with no child hprops, isArgsEq will normally be true. For connectives, reject the match when isArgsEq is false.

5. Support Existential Instantiation: TInstantiate

When YOLO opens hexists or hforall, it must substitute the fresh witness through every operation. Atomic expression fields should be instantiated with the current substitution array.

instance [Embed TCell2 γ] : TInstantiate TCell2 γ where
  change_state _ _ := pure ()

  instantiate x args subst := do
    let st ← get
    let fvars := st.fvars
    let op : TCell2 :=
      { p := x.p.instantiate (fvars.push subst)
        v := x.v.instantiate (fvars.push subst)
        w := x.w.instantiate (fvars.push subst) }
    return hprop.hop
      (Embed.inj op)
      args

If your operation binds variables, follow the TExists/TForall instances: update InstantiateState.fvars in change_state, then rebuild the binder type in instantiate.

6. Define Simplification Semantics: Eval

Eval is the operational heart of a new tag.

class Eval (α : Type) (β : Type) ... where
  evaluate     : α → hprop β → StateRefT (hstate' β) TacticM Unit -- LHS todo
  evaluateWand : α → hprop β → hprop β → StateRefT (hstate' β) TacticM Unit
  evaluateR    : α → hprop β → StateRefT (hstate' β) TacticM Unit -- RHS todo
  evaluateLR   : α → hprop β → StateRefT (hstate' β) TacticM Bool

For many atomic heap predicates, the default atomic behavior is enough:

• on the LHS, move the item from hlt to hla;
• on the RHS, try to cancel it against hla, otherwise keep it in hra;
• in a wand, use evaluateWandDefault;
• in the final LR phase, usually finish by reflexivity or leave a residual goal.

A minimal instance can mirror TAtomic:

instance
    [ToExprT γ]
    [Embed TCell2 γ] [Embed TStar γ] [Embed TWand γ]
    [TIsDefEq γ γ] [TInstantiate γ γ] [Inhabited γ]
    [hStateBasic γ hstate']
    : Eval TCell2 γ (hstate' := hstate') where

  evaluate _ h := do
    let st ← get
    hla.set (h :: hStateBasic.get_hla st)
    hlt.set (hStateBasic.get_hlt st).tail
    tacticScript.push (← `(tacticSeq| apply acc_other_left))

  evaluateWand _ h₁ h₂ :=
    evaluateWandDefault h₁ h₂

  evaluateR _ h := do
    let st ← get
    let rest := (hStateBasic.get_hrt st).tail
    let some (hlaNew, i) ← findIdx (hStateBasic.get_hla st) h
      | do
        hra.set (h :: hStateBasic.get_hra st)
        hrt.set rest
        tacticScript.push (← `(tacticSeq| apply keep_right))
        return
    hla.set hlaNew
    hrt.set rest
    tacticScript.push
      (← `(tacticSeq|
        apply process_cancel_right_ $(Lean.Syntax.mkNumLit (toString i))
        my_simp))

  evaluateLR _ _ := do
    tacticScript.push (← `(tacticSeq| try apply final_left_right))
    return true

The crucial rule: every state mutation in the fast phase must have a matching proof-reconstruction tactic pushed into tacticScript. If you add new behavior, you will usually also add a small reconstruction lemma near the other lemmas in NWO.lean, then push apply your_lemma ....

7. Add The Tag To The Operation Sum

The generic Sum instances already compose ToExprT, HasToHprop, TIsDefEq, TInstantiate, and Eval. Once your tag has the instances above, include it in the type passed to hMain.

The current default elaborator is:

elab "hMain" : tactic =>
  hMain (hstate' := hState_)
    (TStar ⊕ TWand ⊕ TPure ⊕ TEmp ⊕ TAtomic ⊕ TTop ⊕ TForall ⊕ TExists)

With TCell2:

elab "hMain" : tactic =>
  hMain (hstate' := hState_)
    (TCell2 ⊕ TStar ⊕ TWand ⊕ TPure ⊕ TEmp ⊕ TAtomic ⊕ TTop ⊕ TForall ⊕ TExists)

Put more specific tags before TAtomic conceptually: parsing tries registered HasToHprop handlers first and falls back to TAtomic only when none match.

8. Optional: Add Expression Handlers Instead

If your predicate should remain TAtomic but needs special RHS behavior, add an ExprHandler.

def myHandler [Embed TAtomic γ] [hStateBasic γ hstate'] :
    ExprHandler γ hstate' := fun e h => do
  match_expr e with
  | myPredicate a b =>
      -- inspect/update hla/hra/hrt and push reconstruction tactics
      return some ()
  | _ =>
      return none

Then extend HasExprHandlers. The built-in example is hsingleHandler, which recognizes p ~~> v on the RHS and performs pointer-based cancellation.

Experiments

All experiments are in SPLean/Experiments.

• SPLean/Experiments/Misc.lean: small examples, custom language operation syntax, timing instrumentation, and basic YOLO/xsimp' usage.
• SPLean/Experiments/array_findi.lean: array search case study.
• SPLean/Experiments/BiLinInterp.lean: bilinear interpolation case study.
• SPLean/Experiments/cancel100.lean through SPLean/Experiments/cancel800.lean: synthetic cancellation benchmarks of increasing size.
• SPLean/Experiments/GridTheory.lean, SPLean/Experiments/PureThings.lean, and SPLean/Experiments/UnaryCommon.lean: supporting examples and theory snippets used by the experiments.

The root module SPLean.lean currently imports the main experiment files that are built by lake build.