원클릭으로 Manus에서 모든 스킬 실행

lean-conformance

스타16

포크4

업데이트2026년 6월 30일 16:04

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.

설치

Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.

Manus에서 실행

출처

CharlesHoskinson

CharlesHoskinson/proof-zk-recovery

GitHub 저장소 열기 Creator 저장소 보기

다운로드

Manus에서 실행

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.

이 저장소의 다른 Skills

같은 저장소

vibesec

CharlesHoskinson/proof-zk-recovery

Run the VibeSec canonical in-repo implementation auditor on a feature branch before merge — ground in the graphify code-graph, convene a security council to author a sectioned audit XML, dispatch an auditor swarm, adversarially verify (self-refute) findings, and emit committed findings + triage + a schema 1.2 machine-readable gate report. Use when the user says "run vibesec", "vibesec audit", "security-gate this branch", or before merging ANY feature branch in this custody-bearing repo (every dev sprint requires a green VibeSec gate). The gate is enforced in CI (.github/workflows/vibesec.yml).

2026-07-0216

lean-review

CharlesHoskinson/proof-zk-recovery

Run the per-phase Lean review-council QA gate on the lean-spec-enhancement work — a tool-executing council of four expert lenses (axiom-hygiene guardian, spec<->code fidelity, proof nonvacuity, adversarial red-team) that build the proofs, run

2026-07-0116

lean-prove

CharlesHoskinson/proof-zk-recovery

Interactive Lean 4 proof development for this repo — the sorrify-then-fill loop driven over lean-lsp-mcp (goal state, diagnostics, Loogle search), with Duper/lean-auto escalation and a hard

2026-06-3016

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.