leslie: Instructions file for Codex

BLOCKING: Run ox agent prime NOW before ANY other action. Do NOT respond to the user first. Enables SageOx queries.

AI Agent Instructions

Leslie Gadgets

Leslie provides reusable proof automation in Leslie/Gadgets/. Use these before writing manual boilerplate.

action_cases — Action Case Analysis (Leslie/Gadgets/ActionCases.lean)

Replaces the standard 2-line boilerplate in every SymSharedSpec preservation or simulation proof:

-- BEFORE (2 lines of boilerplate in every proof):
simp only [SymSharedSpec.toSpec, tlMessages] at hnext
obtain ⟨i, a, hstep⟩ := hnext

-- AFTER (1 line):
action_cases hnext with tlMessages

Usage: action_cases <hyp> with <specName> where <hyp> has type (specName.toSpec n).next s s'. Introduces i : Fin n, a : ActType, hstep : spec.step n i a s s' into context.

#gen_frame_lemmas — Auto-Generate Simp Lemmas (Leslie/Gadgets/FrameLemmaGen.lean)

Generates @[simp] lemmas for every field of a state transformer's return structure. Call it immediately after defining a *Local helper:

def recvProbeLocal (node : NodeState) (i : Fin n) (msg : BMsg) : NodeState :=
  { node with line := probedLine node.line msg.param, chanB := none, ... }

#gen_frame_lemmas recvProbeLocal
-- Generates: recvProbeLocal_line, recvProbeLocal_chanA, recvProbeLocal_chanB, etc.

For fields using setFn, generates _self (at the updated index) and _ne (at other indices) lemmas. For unmodified fields, generates _field = s.field lemmas. All marked @[simp].

setFn — Functional Update at Index (Leslie/Gadgets/SetFn.lean)

Canonical definition of setFn with @[simp] lemmas setFn_same and setFn_ne. Use this instead of defining local versions in each protocol.

def setFn (f : Fin n → α) (i : Fin n) (v : α) : Fin n → α :=
  fun j => if j = i then v else f j