pegrex-verify

Files (1)

• SKILL.md

SKILL.md (first lines)

# verification

- `verify_patch(before.py, after.py)` -> {"verified": bool,
  "counterexample": {"inputs": {...}}} | None. NEVER trust an edit that
  was not verified; a counterexample is a gift, not a failure.
- `semantic_diff(a.py, b.py)` compares path contracts, not lines.
  `refine.discharge_source` checks `# requires:` / `# ensures:` comments.
- Repair loop: `cegis.repair(src, proposer)` feeds counterexamples back
  to the proposer until verified or the budget is spent.
- Three-valued everywhere: wrap results with `tv.wrap` -- a crash, a
  timeout, or a missing result is UNKNOWN, never proved.
- Inspect `python pegrex.py soundness --language ID` before interpreting a
  result. Its manifest states the supported fragment and unsupported cases;
  parser availability and process completion are not proof.
- Use `PathEnumerator.enumerate_bounded()` and
  `LinearBackend.entails_with_status()` for resource-aware verification. A path
  cap, solver query/deadline budget, or per-file timeout yields UNKNOWN and no
  partial path set; legacy boolean entailment fails closed.
- Security scans are evidence reports, not proofs of safety. Preserve their exact
  source, rule-catalog, parser, and OSV snapshot identities. Offline OSV misses
  are UNKNOWN; SARIF suppressions require a reviewer justification and remain
  visible to audit rather than erasing the finding.

## Proof-gated edits and independent checking
- `apply_patch_gated` stages candidates, checks canonical equivalence certificates
  through `pegrex.kernel`, enforces required invariants and security policy, runs
  argv-only tests, and atomically applies only approved edits.
- `repair_and_recheck` reruns the same analyzer in staging; the target finding
  must decrease and no other finding identity may increase.
- `EditAudit` preserves original/proposed source, diff, tests, proofs, and the
  approval decision for both accepted and rejected attempts.
- The minimal kernel accepts only bounded canonical contract-set equality proofs.
  It does not execute counterexamples or trust the broad analyzer's verdict.

## Analyzer negative controls
- `standard_negative_controls()` deliberately weakens parser, solver, and rule
  behavior. Require all controls to be killed; a bad baseline is UNKNOWN and a
  surviving weakened analyzer is a failed control, not a passing test suite.

From ovoxnox/pegrex, MIT.

More from ovoxnox/pegrex