Updating verification-algorithm.md

[jyoo980]

No description provided.

[coderabbitai]

📝 Walkthrough

Walkthrough

This PR modifies the proof verification algorithm to refine how backtracking and spec verification are handled. It narrows the ProofState workstack invariant to apply only during backtracking pushes, adds an assume_without_verification flag to WorkItem to indicate when regenerated specs should be assumed without verification, and refactors the step() function to unpack this flag and conditionally skip verifier calls. The workstack evolution logic is also updated to depend on specc.next_step using pattern matching rather than inspecting the LLM conversation's response text, with explicit handling for BACKTRACK_TO_CALLEE that propagates the assumption flag when backtracking to external callees.

Possibly related PRs

• Updating backtracking strategy for functions outside of projects #144: Modifies the same proof-state stepping and backtracking logic, including branching on spec_conversation.next_step, handling BACKTRACK_TO_CALLEE with callee lookup, and propagating assumption behavior through WorkItem.

Suggested reviewers

• mernst

🚥 Pre-merge checks | ✅ 3

✅ Passed checks (3 passed)

Check name	Status	Explanation
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch yoo/sync-algorithm-doc

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 4

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@verification-algorithm.md`:
- Around line 196-203: The loop reassigns the local variable specc when
call_llm_for_next_step(...) returns a new SpecConversation but never writes it
back into pruned_speccs, leaving the list with a stale object; change the
iteration to preserve the updated object (e.g., iterate with index or replace
the element after modification) so that when you call call_verifier(),
call_llm_for_next_step(), set specc.next_step = ACCEPT_VERIFIED_SPEC, or later
do match specc.next_step, the list contains the updated SpecConversation; update
the code around pruned_speccs, the for-loop, and assignments to specc (and
references to call_llm_for_next_step, call_verifier, is_success,
ACCEPT_VERIFIED_SPEC) to write the modified specc back into pruned_speccs.
- Around line 110-112: The invariant text uses inconsistent terminology —
replace all occurrences of backtrack_hint and mixed “non-empty/non-None”
phrasing with the canonical WorkItem field name hint and a consistent nullness
check; e.g., state: “Invariant: all WorkItems with a non-None hint are above all
WorkItems with hint == None on the workstack” and update any nearby mentions to
use hint and non-None uniformly (referencing the WorkItem type and the workstack
invariant).
- Around line 186-187: The call to prune_heuristically uses three arguments (fn,
new_speccs, proofstate) while the documented signature is
prune_heuristically(fn, speccs), causing a mismatch; fix by either (A) updating
the function definition of prune_heuristically to accept the extra proofstate
parameter and use it inside the implementation (and update the documented
signature to prune_heuristically(fn, speccs, proofstate)), or (B) change the
call site to match the two-arg API by passing only (fn, new_speccs) and removing
proofstate usage at that call; ensure the chosen API (function implementation,
all call sites, and the documented signature) is made consistent and reference
prune_heuristically, fn, new_speccs, proofstate, and speccs when applying the
change.
- Around line 183-185: The doc incorrectly shows tuple unpacking of a WorkItem
instance; update the snippet to use attribute access instead: retrieve the top
WorkItem via proofstate.workstack.top() and access its fields like
work_item.function, work_item.hint (or work_item.backtrack_hint), and
work_item.assume_without_verification, then pass those to
generate_and_repair_spec to produce new_speccs: List[SpecConversation]; ensure
variable names match the WorkItem dataclass field names used in the
implementation.

🪄 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: fcd249a4-3833-4040-b280-a73c5deda736

📥 Commits

Reviewing files that changed from the base of the PR and between 1e0c381 and 3639ea5.

📒 Files selected for processing (1)

• verification-algorithm.md