lean-conformance

Sterne16

Forks4

Aktualisiert30. Juni 2026 um 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.

Installation

Mit Codex oder Claude installieren Kopieren Sie diesen Prompt, fügen Sie ihn in Codex, Claude oder einen anderen Assistant ein und lassen Sie die Skill-Seite prüfen und installieren.

In Manus ausführen

Quelle

CharlesHoskinson

CharlesHoskinson/proof-zk-recovery

GitHub-Repository öffnen Creator-Repositorys ansehen

Download

In Manus ausführen

Verwandte BerufeSOC

Basierend auf der SOC-Berufsklassifikation

SoftwareentwicklerInformatik- und Mathematikberufe·SOC 15-1252

Datei-Explorer

6 Dateien

SKILL.md

readonly

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.

Mehr aus diesem Repository

gleiches Repository

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.