lean-conformance

name	lean-conformance
description	Property-based spec<->code conformance for this repo — regenerate Lean-emitted vectors (lake exe vectorgen), replay them against Recovery.Logic with the Haskell tasty-hedgehog suite, and run the mutation sweep (each single-guard mutation must fail at least one vector). Use when validating that the Lean spec still verifies the Haskell implementation, or when the review council's fidelity/adversarial lenses need conformance evidence.
argument-hint	[regen | run | mutate]

Lean Conformance

The executable Lean spec is the test oracle for Recovery.Logic. Set SKILL=skills/lean-conformance.

Operations (references/harness.md)

• regen: lake exe vectorgen -> lean/Conformance/vectors/*.jsonl (Lean is the oracle; no hand-maintained expected values).
• run: cabal test redemption-conformance -> replays vectors vs Recovery.Logic; disagreement is a real bug in one implementation.
• mutate: scripts/ci/lean-mutate.sh applies single-guard mutations to a throwaway copy of Recovery.Logic; each MUST fail >=1 vector. A surviving mutant = a coverage hole.

NOTE: the vectorgen exe + ConformanceSpec.hs + lean-mutate.sh are built in Phase 2; this skill is the operating contract the council and the Phase-2 plan share.

Guardrails

• Mutations run on a throwaway copy; the tree is restored. Commits: terse, no AI attribution.