| 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.
