Hill-climb property generation quality

Goal

Improve property-generation prompts so they produce more valid, interesting properties with fewer property-level false positives.

This is a follow-up to #79. Property provenance must land first so outcomes can be attributed to the exact source lens/framework and generated property.

Definitions

• Valid property: consistent with the target protocol's intended behavior, reachable, non-vacuous, and expressible as an observable oracle.
• Interesting property: project-specific and capable of detecting a meaningful state violation rather than restating a generic or duplicate assertion.
• Property false positive: a generated property that would flag intended protocol behavior as a violation.

V1 scope

1. Define a structured adjudication record keyed by the canonical property ID from #79:
   • property_id
   • valid | invalid | needs-review
   • interesting: boolean
   • false_positive: boolean
   • rationale
2. Aggregate valid rate, interesting rate, and false-positive rate by source lens/framework.
3. Define a deterministic score for comparing a candidate property-generation prompt against its baseline.
4. Run candidates against a fixed, pinned benchmark cohort for multiple trials.
5. Accept a candidate only when it improves the aggregate score without increasing the false-positive rate; otherwise retain the baseline.
6. Preserve the candidate prompt/config, benchmark lineage, per-property adjudications, aggregate score, and accept/reject decision as artifacts.

Non-goals

• Property provenance itself; that belongs to #79.
• Changing invariant fuzzer selection or scheduling.
• Automatically changing target production code.
• Optimizing downstream finding triage.

Acceptance criteria

• A fixed benchmark cohort and trial count can be configured.
• Baseline and candidate runs use compatible benchmark and scoring lineage.
• Each adjudicated property links to its canonical property ID and source provenance from #79.
• Reports show valid, interesting, and false-positive rates overall and per source lens/framework.
• Candidate acceptance is deterministic from the recorded inputs and scoring rule.
• Rejected candidates do not replace the active property-generation prompt.
• Tests cover improved, regressed, tied, and incomplete-adjudication outcomes.
• Documentation explains the scoring rule, artifacts, and how to reproduce an optimization run.

Dependency

Blocked by #79.

Start with the dependency on issue #79, since property provenance and canonical property IDs must be available first. Use the V1 scope and acceptance criteria to define the benchmark, adjudication, scoring, artifact, and decision requirements; done means the listed improved, regressed, tied, and incomplete-adjudication outcomes are tested and the optimization process is reproducible.