feat: vera/proposeEdit enforced edit workflow (#222 Phase F1)#721
Merged
Conversation
The first skill-layer workflow: edit -> verify -> apply as one LSP method. The proposed text runs through the Phase E speculative verify; the gate applies iff the proof delta has no newly_undischarged obligations and no error diagnostics (force: true overrides both, loudly). On apply: workspace/applyEdit, canonical DocumentStore update, diagnostics republish; the client's echoed didChange replays from the warm discharge cache. On refuse, canonical state untouched. New vera/lsp/workflows.py separates the pure decision (propose_edit) from the effectful orchestration (apply_propose_edit); 12 new tests (gate, force overrides, wiring against a structural fake server, full-document-range goldens). Release prep for v0.0.166; ROADMAP regains a Phase F row while the reopened issue is in flight. Co-Authored-By: Claude <[email protected]>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (5)
📝 WalkthroughWalkthroughPhase F1 adds ChangesPhase F1 proposeEdit Skill-Layer Workflow
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #721 +/- ##
=======================================
Coverage 90.95% 90.96%
=======================================
Files 69 70 +1
Lines 24676 24727 +51
Branches 292 292
=======================================
+ Hits 22444 22492 +48
- Misses 2225 2228 +3
Partials 7 7
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@tests/test_lsp.py`:
- Around line 703-757: Add a failing-client branch in the tests by extending
_FakeServer.workspace_apply_edit to simulate applied=False and then add a test
case in TestProposeEditWiring that calls apply_propose_edit and asserts the
client-refusal path: ensure out["applied"] is False, server.applied_edits
remains empty, server.published stays [], the store (server.store.get(URI))
still contains SPEC_BASE with original version, and server.analyses[URI] is
unchanged; reference the existing apply_propose_edit call pattern used in
test_refuse_path_touches_nothing to mirror expectations for the client-declines
scenario.
In `@vera/lsp/server.py`:
- Around line 177-182: The crash occurs because "getattr(params, 'text', None)
or params.get('text')" evaluates params.get(...) even when params has no .get
and text == "" (falsy), causing AttributeError; update the uri and text
extraction to first check for .get and prefer params.get(...) with a fallback to
getattr, or if .get is missing use getattr only (e.g. if hasattr(params, 'get'):
uri = params.get('uri', getattr(params, 'uri', None)) else: uri =
getattr(params, 'uri', None); do the same for text), leaving the existing force
handling and the final call to apply_propose_edit(server, uri, text,
bool(force)) unchanged so apply_propose_edit always receives a proper str for
text.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: dd881936-7d9b-4738-bffc-cc51ac844787
⛔ Files ignored due to path filters (5)
docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**uv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (10)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdpyproject.tomltests/test_lsp.pyvera/README.mdvera/__init__.pyvera/lsp/server.pyvera/lsp/workflows.py
CodeRabbit flagged the getattr-or-get pattern in both custom handlers: a falsy-but-present value (text="", a legitimate replace-with-empty- document) fell through to .get on pygls' attribute-style params and raised AttributeError. Both vera/proposeEdit and vera/speculativeEdit now extract via _param(), which decides membership with a sentinel, never truthiness; regression tests cover the SimpleNamespace empty-text case. Also pins the documented fire-and-forget applyEdit semantics: the fake server now returns a resolved Future carrying the client's verdict, and a client-refusal test asserts canonical state is NOT rolled back (the response's applied reports the gate verdict; a declining client re-converges on its next full-sync didChange). Co-Authored-By: Claude <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@vera/lsp/server.py`:
- Line 197: The current assignment force = bool(_param(params, "force")) treats
strings like "false" as true; replace this with an explicit strict boolean parse
using the raw value from _param(params, "force") (e.g., let v = _param(params,
"force") and set force = True if v is the boolean True or if str(v).lower() in
{"true","1","yes"} else False) so only legitimate truthy boolean representations
enable the force path; update the code that reads the force variable (the
assignment using _param and any downstream checks) to use this strict parse.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: b29b0565-6f65-4141-882b-4b607819a60b
📒 Files selected for processing (6)
README.mdROADMAP.mdTESTING.mdtests/test_lsp.pyvera/lsp/server.pyvera/lsp/workflows.py
CodeRabbit flagged bool(_param(params, "force")): generic truthiness makes a malformed payload like force="false" (string) bypass the verification gate — the one bit whose whole purpose is to be hard to skip, failing in the open direction. _force_param() now engages only on boolean True; strings, numbers, and other malformed values fail closed to a refused edit with an explanatory delta. Co-Authored-By: Claude <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@vera/lsp/server.py`:
- Around line 208-212: The handler must validate that params contain non-empty
strings for "uri" and "text" before delegating to apply_propose_edit; update the
code that calls _param (the variables uri and text) to perform strict type and
emptiness checks (e.g., isinstance/str and len>0) and short-circuit by returning
a refused response shape if validation fails. Keep using the same helpers
(_param, _force_param) and the same call to apply_propose_edit(server, uri,
text, _force_param(params)) only when validation passes; do not propagate None
or non-str values into apply_propose_edit.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 7c621dfc-e8ac-4ac3-b1ce-015c42d9ceb8
📒 Files selected for processing (5)
README.mdROADMAP.mdTESTING.mdtests/test_lsp.pyvera/lsp/server.py
…round 3) Missing or non-string uri/text in vera/proposeEdit and vera/speculativeEdit payloads previously flowed into the parse pipeline as None and surfaced as opaque JSON-RPC internal errors. _require_str() now fails closed at the protocol boundary with JsonRpcInvalidParams (-32602), the JSON-RPC-native refusal; the empty string stays valid (present value, replace-with-empty- document). Tests pin both directions. Co-Authored-By: Claude <[email protected]>
This was referenced Jun 11, 2026
Closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Phase F1 of the issue 222 skill layer:
vera/proposeEdit, the first enforced workflow method — the whole edit → verify → apply sequence runs server-side as one LSP request, so an agent cannot apply an unverified edit. Applying is the final step of verifying.Per the Phase F design comment (2026-06-11):
vera/lsp/workflows.py—propose_edit()is the pure decision (speculative verify via the Phase E machinery + the gate);apply_propose_edit()is the effectful orchestration. The gate: apply iff the proof delta has nonewly_undischargedobligations AND the proposed state has no error diagnostics;force: trueoverrides both, loudly (the response still carries the full delta).workspace/applyEditserver→client request (the client owns the buffer — the server round-trips the edit rather than silently diverging), canonicalDocumentStoreupdate, re-analysis + diagnostics republish. The client's echoeddidChangereplays from the warm discharge cache — the pre-warming Phase E was designed for.vera/speculativeEdit.create_server(); wire glue only.Verification gate semantics
Locking: the decision runs under
analysis_lock(one Z3 session, strictly serialised); the apply path releases beforeanalyze_and_publishre-acquires —threading.Lockis not reentrant, and the second pass replays from cache by construction.Tests (12 new; 4,284 total)
newly_dischargedmust not block); breaking edit refused (violatednat_subsurfaced); non-compiling edit refused; force overrides the proof gate AND the error gate with the delta still reported.full_document_rangegoldens: trailing-newline virtual line; UTF-16 end column on the astral-plane fixture.Release prep (v0.0.166)
Version across all 6 tracked sites, CHANGELOG section + compare links, ROADMAP regains a Phase F row (issue 222 is open again and must be tracked; the F3 PR removes it), TESTING.md/README counts, module map (lsp/ 829 → 1007 lines), site assets regenerated.
Part of the Phase F arc (F1 → F2
strengthenContract→ F3addEffect); this PR intentionally does not affect the issue's open state.🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Documentation
Tests