Skip to content

v0.0.167

Choose a tag to compare

@aallan aallan released this 11 Jun 14:54
· 310 commits to main since this release
6ee74b6

Added

  • #222 Phase F2 — vera/strengthenContract, the contract-change workflow with a call-site audit: {uri, fn, kind: requires|ensures, expr} locates the first clause of that kind on the named top-level function, splices the new expression over the clause's span in the canonical document, and runs the candidate through the proposeEdit pipeline. The audit is the proof delta itself — a tightened precondition some caller no longer satisfies surfaces as newly_undischarged call_pre items at the call sites (Phase A keys obligations by call-site span precisely for this) and the gate refuses; a strengthened postcondition the body proves discharges and applies. No force parameter — the dedicated workflow exists to make the audited path the easy one (an agent that wants to push through a breaking change can construct the full text and call vera/proposeEdit with force explicitly). Requests that cannot name a splice target (unknown function, unopened or unparseable document, bad kind) refuse with JSON-RPC InvalidParams at the boundary.